Cleaning, renaming obscure functions and documenting in Hashcons.

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


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15835 85f007b7-540e-0410-9357-904b9bb8a0f7
Reusing the Hashset data structure in Hashcons. Hopefully, this should
not disrupt anything...

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15837 85f007b7-540e-0410-9357-904b9bb8a0f7
Ltac repeat is in fact already doing progress

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15838 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a new tactical infoH tac, that displays the names of hypothesis created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15839 85f007b7-540e-0410-9357-904b9bb8a0f7
Use the library function List.substract in prev commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15840 85f007b7-540e-0410-9357-904b9bb8a0f7
New makefile shortcuts miniopt and minibyte for coqtop + plugins

 They are meant to quickly check that all the ml code of coqtop
 and its plugins is compilable

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15841 85f007b7-540e-0410-9357-904b9bb8a0f7
avoid referring to Term in constrexpr.mli and glob_term.mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15842 85f007b7-540e-0410-9357-904b9bb8a0f7
Argextend: avoid useless "open Extrawit"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15843 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove some more "open" and dead code thanks to OCaml4 warnings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove some dead code in the vm

 Apparently Cysmtable.set_global_boxed is unused,
 and removing it allows to get rid of a bunch of C code
 concerning "boxed" things (including ACCUMULATECOND
 instruction).

 Still TODO: Csymtable.set_transparent_const and
 Csymtable.set_opaque_const appear to be no-ops.
 Should we remove them ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15845 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove the unused "intel" field in Proof.proof_state

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15846 85f007b7-540e-0410-9357-904b9bb8a0f7
Moved Compat to parsing. This permits to break the dependency of the
kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.

This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
Adding a nominal typing layer to Metasyntax in order to clarify
things up. Records are used instead of their equivalents as tuples.
This is maybe syntactically heavier, but this is semantically
equivalent and easier to understand.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
Getting rid of Compat in the checker.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15849 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefile.build: easier compilation with timings info

 On a reasonable platform equipped with a /usr/bin/time, a simple
 "make TIMED=1" should provide you with timings of the .v compilations.

 If you don't have /usr/bin/time, or prefer a different output format,
 you can still do a "make TIMECMD='...'".

 For storing the timings in a spreadsheet, simply do:
 "make TIMED=1 2> timings.csv"
 and then import this csv in your favorite office program,
 with whitespace as separator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15850 85f007b7-540e-0410-9357-904b9bb8a0f7
En cours pour bug 2836

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15851 85f007b7-540e-0410-9357-904b9bb8a0f7
En cours pour 'generalize in clause' et 'induction in clause'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15852 85f007b7-540e-0410-9357-904b9bb8a0f7
Improving error message when abtraction over goal (abstract_list_all
used when applying schemes - induction, rewrite, ...) is well-typed
but not of the right type.

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