coq/test-suite/parser, branch master

Remove interface plugin

2009-12-02T08:36:14+00:00

It has moved to the contribs (Sophia-Antipolis/Interface).

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

Remove the barely-used/obsolete/undocumented syntax "conditional rewrite"

2009-07-24T13:27:45+00:00

I wonder how many of us were aware of the existence of such syntax ;-)
Anyway, it is now subsumed by "rewrite by".

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

Achèvement suppression traducteur dans contrib/interface

2005-12-26T17:05:45+00:00

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

Consequence of allowing the numerical argument of auto to be an ident for ltac

2005-05-23T13:13:33+00:00

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

Re-commit version nouvelle syntaxe

2004-11-28T18:20:57+00:00

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

Passage à la v8 pour test parser

2004-11-28T16:34:48+00:00

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

the output the parser should produce now

2004-03-06T08:00:30+00:00

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

Add an example with Ring.

2002-12-09T13:59:39+00:00

Modified obj_magic.out because some formulas changed representation.


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

correcting the treatment of many tactics that use quant_hyp in file xlate.ml

2002-10-06T20:59:04+00:00

and associated file.  Also adding a systematic check approach


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