aboutsummaryrefslogtreecommitdiff
path: root/test-suite/parser/obj_magic.out
AgeCommit message (Collapse)Author
2009-12-02Remove interface pluginglondu
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
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
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
2004-03-06the output the parser should produce nowbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5438 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Add an example with Ring.bertot
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
2002-10-06correcting the treatment of many tactics that use quant_hyp in file xlate.mlbertot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:33:13 +0000