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
Suggest to use clean rather than archclean before recompiling.
For instance, generated files depend on whether configuration is done
with dynlink or not and they should be cleaned.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15854 85f007b7-540e-0410-9357-904b9bb8a0f7
Repaired configure damaged in r15748 for those bash users which have
CDPATH variable set. Indeed, command cd is verbose when CDPATH is set,
what would introduce garbage in the generated file config/coq_config.ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15855 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "En cours pour 'generalize in clause' et 'induction in clause'"
Sorry, was committed mistakenly.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15856 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert r15851 "En cours pour bug 2836".
Sorry, was committed mistakenly.

This reverts commit e9cb84af469519b824899c047eed1fed2f8d5af6.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15857 85f007b7-540e-0410-9357-904b9bb8a0f7
More accurate timings for "Time foo"

 The elapsed time in seconds was computed via a difference of Unix.time(),
 but these Unix.time() aren't precise enough (just a number of seconds),
 and a difference is hence even less precise.  We now use Unix.gettimeofday,
 and round the time difference to the millisecond.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15858 85f007b7-540e-0410-9357-904b9bb8a0f7
coqtop -time : display per-command timings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7
Repair the configure after Hugo's last "repair" ;-)

 Ok, I wasn't aware of the funny behavior of cd in presence of $CDPATH.
 But the last "repair" was worse, trying to write into non-existing file
 theories/config/coq_config.ml

 Things should be better now:

 * no more Coq_config.theories_dirs at all, since it was completely unused :-)

 * concerning Coq_config.plugins_dirs, we list them without any "cd" into plugins,
   hence keeping the "plugins/" part in their paths, and adapt accordingly
   the only use (!) of plugins_dirs, in coq_makefile

 Please run ./configure again after upgrading to this commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15860 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix a confusion between types of locations in an untyped part of the parser
after the migration of compat.ml4

 This was leading to huge positions written to .glob files, making
 coqdoc loop forever.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15861 85f007b7-540e-0410-9357-904b9bb8a0f7
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box

 Nested was never constructed, while the notion of abstract_tactic_box
 is obsolete (cf. Refiner.abstract_tactic).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
Clean-up : no more Proof_type.proof_tree

 Btw, remove unused code in the xml plugin and in Tactic_printer

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
Proof_type: rule now degenerates to prim_rule

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7
Clean-up : removal of Proof_type.tactic_expr

 This instance of gen_tactic_expr was used only to decorate
 tactics via Refiner.abstract_tactics and alii, but these
 expressions are now ignored by the new proof-engine (no "info"...).

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