coq/scripts, branch master

coqc and coqmktop migrated in tools/, get rid of scripts/ subdir

2013-04-18T16:56:17+00:00

 No need to place these binaries apart, and anyway they aren't
 (shell) scripts since ages.

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

Coqc: accept -exclude-dir + some others + cleanup (fix #3025)

2013-04-18T16:56:03+00:00

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

Coqmktop: dynlink is now mandatory due to Maxime's native-compiler

2013-04-17T16:25:43+00:00

 Some cleanup btw, for instance Dynlink.init is deprecated since at least
 ocaml 3.11

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

Restrict (try...with...) to avoid catching critical exn (part 13)

2013-03-13T00:00:49+00:00

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

Restrict (try...with...) to avoid catching critical exn (part 11)

2013-03-13T00:00:37+00:00

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

Fixed parsing of -no-native-compiler flag.

2013-01-24T09:46:54+00:00

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

Revert "remove -rectypes except for term.ml"

2013-01-22T14:18:38+00:00

Preparing landing of the native compiler, which requires -rectypes flag.

This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1.



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

Coqmktop and camlp4 : sequel to commit 16113

2013-01-12T19:08:18+00:00

 Actually I don't see any reason to link q_utils and q_coqast
 in coqtop.byte specifically when using camlp4 (and not camlp5).

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

Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.

2012-12-22T05:10:11+00:00

Also fixing coqmktop for use with Camlp4. Don't know if this is the
fix intended by coqmktop experts or not, though.

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

Ensure that a function declared with a label is used with it

2012-12-08T23:33:33+00:00

 This correspond to ocaml4 warning 6

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