fix r15860 : no slash after $(COQLIB)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
When loading a plugin, prefer .cma to .cmo

Imagine foo.cma contains foo_utils.cmo and foo.cmo.
Also imagine that foo.cmo depends on foo_utils.cmo.
With this patch, when asked to load foo, Coq loads the foo.cma archive.
Loading simply foo.cmo would fail since foo_utils.cmo is needed to load
foo.cmo.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15883 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 introduced bug #2709 on duplicate entries in index and tentative fix of it in r15053 mixed up names of files and names of constants in index (as reported by P. Castéran on coqdev).

Patch by Hugo Herbelin :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15885 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefile.build: $(MLINCLUDES) out of $(OPT/BYTEFLAGS)

Allow to erase special $(CHKFLAGS)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15886 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefiles: Only -I required dirs (config, lib, ide) when compiling coqide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15887 85f007b7-540e-0410-9357-904b9bb8a0f7
Coq_makefile: easier compilation with timings info (from r15850)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
Stylistic improvement: avoid a "if match List.hd"

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15890 85f007b7-540e-0410-9357-904b9bb8a0f7
Continue killing hidden tactics : no more generated h_xxx

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15891 85f007b7-540e-0410-9357-904b9bb8a0f7
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