aboutsummaryrefslogtreecommitdiff
path: root/test-suite/modules/PO.v
AgeCommit message (Collapse)Author
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
The manual was already saying that it was deprecated, but no warning was emitted. Fixes #10572
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 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
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
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4449 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-05Corrige Bug (PR#290)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3989 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3635 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:58:47 +0000