coq/contrib/interface, branch master

Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

2009-03-20T01:22:58+00:00

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

Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"

2009-03-16T08:18:53+00:00

now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
etc.). The terminology for clauses (though I don't find the term
"clause" very intuitive after all) is mostly preserved except for
"simple_clause" which becomes a light form of "clause" instead of
being an atom of clause (what played the role of "simple_clause" is
now called "goal_location" - better names are welcome).
Main changes are in tacticals.ml and tactics.ml.



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

Cleaning/uniformizing the interface of tacticals.mli

2009-03-14T21:29:19+00:00

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

Makefile: ml dependencies of contribs are moved to .mllib files

2009-03-14T11:29:46+00:00

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

fixed groebner as a plugin + pattern matching Timeout

2009-03-06T21:40:38+00:00

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

coq-interface and coq-parser can be calls to coqtop with adequate code dynlink

2009-02-20T13:39:46+00:00

 From files in contrib/interface, we create (if natdynlink is available) two
 plugins named coqinterface_plugin.{cma,cmxs} and coqparser_plugin.{cma,cmxs}.
 These plugins are loaded respectively by CoqInterface.v and CoqParser.v.
 So coq-interface can be "coqtop -require CoqInterface", and coq-parser can be
 "coqtop -batch -l CoqParser" (this one cannot be compiled into a .vo, otherwise
 a customized toplevel is launched during the compilation). Turing coq-interface
 and coq-parser and their .opt versions into shell scripts allow to spare around
 40 Mb of disk space...

 Nota: at dynlink, parse.ml was conflicting with the module Parse of the ocaml
 runtime, so I renamed it into coqparser.ml

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

pushed evar reduction in kernel

2009-02-06T21:25:52+00:00

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

Forgot a file in r11859. Sorry...

2009-01-27T11:42:55+00:00

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

Les records déclarés avec Record ne peuvent plus être récursifs (le

2009-01-19T19:17:09+00:00

comportement est similaire à la 8.1). Les records récursifs peuvent-être 
déclarés avec Inductive et CoInductive, avec les effets idoines sur leur 
nature.

J'ai fait quelques changements dans VernacInductive pour que tout ceci 
fonctionne bien ensemble. Il reste du nettoyage à faire et probablement 
des ajustement dans le Printing.



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

- Structuring Numbers and fixing Setoid in stdlib's doc.

2009-01-19T11:05:02+00:00

- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True").



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