aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/RecTutorial.v
AgeCommit message (Collapse)Author
2011-02-21Some fixes of the test-suite scriptsletouzey
In particular, the Fail meta-command cannot for the moment catch a Syntax Error, which is raised by Vernac.parse_sentence, before we even now that the line starts by a Fail... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
Definition's is not so painless. It seems to however generally provide "nicer" scripts so let us keep it and update the contribs and test-suite accordingly. Also enforced that the actual introduced names to be exactly as given in the statements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28Adaptation au passage de vector dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8869 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-23Répercussion mise à jour de Pierre Casteran vis à vis du changement de ↵herbelin
statut du paramètre de Acc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7921 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-21 15:50:17 +0000