coq/contrib/interface/vernacrc, 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

Now, the grammar extension from .v files are concentrated in just a few

2004-01-14T14:52:59+00:00

files.


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

Integrating the Ltac language and the Blast tool into the interface

2001-12-18T14:02:29+00:00

capabilities:

The Ltac language is the language that makes it possible to define new tactics
without using the ocaml language (already present in coq for a few months).

The Blast tool is a tool that checks whether the goals could be solve
automatically and proposes the proof trace to the user.


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

These files are used to construct an independent parser, that is a small

2001-04-04T13:03:53+00:00

coq that is only able to parse coq script files and produced a tree-like
representation.  For now this representation is only given in a postfix format,
but other format (such as XML) could also be possible.


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