aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/Inversion.v
AgeCommit message (Collapse)Author
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2019-05-23Fixing typos - Part 3JPR
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
2014-09-11Other bugs with "inversion as" (collision between user-provided names and ↵Hugo Herbelin
generated equation names).
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced.
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-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-04Removal of trailing spaces.serpyc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Fixed a bug in the interaction between dEqThen and inject_at_positionsherbelin
which was disturbing inversion and sometimes making it failing in presence of dependent equalities (injection still doesn't know how to split dependent equalities, resulting in a smaller number of equalities than expected for dEqThen). [also restored inv.ml as it was before 12356 which uselessly and inadvertently modified it] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12360 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
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09- Correction erreur dans test output Notation.vherbelin
- Ajout test pour non-régression du bug #1968 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 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
2005-03-21Ajout Unset Implicit Arguments manquantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-20Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des ↵herbelin
hyps dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-13Nouvel exemple; correction du contexte du précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5475 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Correctionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout vieil exemple de coq-clubherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5458 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout bug #540herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5452 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-06Test de la correction d'un bug soumis par Dachuan Yuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3217 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:42:27 +0000