Removed dead code about linking Module names in coqdoc.
Code was probably unused since scan_file made obsolete in r11024.
See also r12890.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15892 85f007b7-540e-0410-9357-904b9bb8a0f7
Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.
Indeed r15885 still had problems (index contained referenced objects and not
only defined objects, sorry).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15893 85f007b7-540e-0410-9357-904b9bb8a0f7
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing redundant definition of case_eq (see #2919).
Thanks to F. Blanqui for spotting it out.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15897 85f007b7-540e-0410-9357-904b9bb8a0f7
univ inconsistency error message gives evidence of a cycle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
Using weak tables instead of plain hash tables while hashconsing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
Taking into account that ocamlfind might find a package w/o the files
needed for compiling being present. Do the check by hand. Incidentally
improved reporting messages. Also check gSourceview.cmi rather than
gSourceview.mli for better guess that lablgtk sourceview bindings are
there (I've seen installations where gSourceview.mli was here but not
gSourceview.cmi).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15901 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix test-suite output/* in bench

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
Cygwin gcc do not accept -mno-cygwin anymore

As far as I understand, the standard gcc in cygwin is not able anymore to build
non cygwin executable. There is instead a special package with a special gcc that
compiles executable that can be used out of cygwin.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15907 85f007b7-540e-0410-9357-904b9bb8a0f7
Do not install libcoqrun.so if compiled with -custom

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15908 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefile.build: CONFIG is now in clib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15909 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide does not need dllcoqrun.so

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15914 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix bug #2892

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15916 85f007b7-540e-0410-9357-904b9bb8a0f7
RefMan-tac: fix a few glitches concerning the documentation of eqn:

 These were introduced during Guillaume's backport to trunk of its
 improved tactic documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15920 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide for Gtk-mac-integration 2.0.0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15922 85f007b7-540e-0410-9357-904b9bb8a0f7
Text inserted by insert_this_phrase_on_success correct tagging

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15923 85f007b7-540e-0410-9357-904b9bb8a0f7
 the new .dir-locals.el thanks to Pierre Courtieu

As it says :
Set default directory to coq root ONLY IF variable
coq-project-find-file is non nil. This should remain a
user preference and not be set by default. This setting
is redundant with compile-command above as M-x compile
always CD's to default directory. To enable it add this
to your emacs config: (setq coq-project-find-file t)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15924 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqmktop: missing -I (fix #2851)

 The modules used in coqmktop's temporary main file should have
 their .cmi in the search path, hence a small set of -I is required:
 lib, toplevel. We do not place their the full list to avoid issues
 with the win32 command-line length

 Btw, coqmktop -boot now also builds its list of -I instead of receiving
 them via its command-line, it's simpler this way...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
Cleared a purely declarative .ml file and moved its interface to intf/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
Removed a few calls to "Opaque" in Logic.v ineffective since at least
V7.1. Thanks to Assia for reporting.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15929 85f007b7-540e-0410-9357-904b9bb8a0f7