Error: The file ssreflect.vo contains library ssreflect and not library theories.ssreflect

After installing ssreflect, its libraries for Coq are installed in /usr/local/lib/coq/user-contrib/theories. When ever I want to import libraries of ssreflect in CoqIDE (ssrcoqide), I get the following error messages:
Error: The file /usr/local/lib/coq/user-contrib/theories/ssreflect.vo
  contains library ssreflect and not library theories.ssreflect
Error: The file /usr/local/lib/coq/user-contrib/theories/eqtype.vo
  contains library eqtype and not library theories.eqtype
......

There are two ways to solve this problem.  I don't know which one is better.

Method 1

Move all the ssreflect libraries for Coq from /usr/local/lib/coq/user-contrib/theories to /usr/local/lib/coq/user-contrib.

Method 2

Add "-I /usr/local/lib/coq/user-contrib/theories" to launch ssrcoq and ssrcoqide. Actually, I rename ssrcoq and ssrcoqide to ssrcoq.opt and ssrcoqide.opt respectively, and use the following two scripts to launch them.

The script /usr/local/bin/ssrcoq:
#!/bin/bash

/usr/local/bin/ssrcoq.opt -I /usr/local/lib/coq/user-contrib/theories $*

The script /usr/local/bin/ssrcoqide:
#!/bin/bash

/usr/local/bin/ssrcoqide.opt -I /usr/local/lib/coq/user-contrib/theories $*

0 意見: