aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/refine.v
AgeCommit message (Collapse)Author
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
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.
2017-08-21Fixing another regression with 8.4 wrt to βι-normalization of created hyps.Hugo Herbelin
This one is a continuation of e2a8edaf59 which was βι-normalizing the hypotheses created by a "match". We forgot to do it for "let" and "if". This is what this commit is doing.
2015-12-15Fix test-suite files after change in refine tactic.Maxime Dénès
Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 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-11-04Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)herbelin
Grant wish #1988 ("fun" forces reduction in "refine" if needed) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11536 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-18Wish #1582 (3eme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9838 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-10Correction d'un bug refineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9359 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05Vieux bug de fin 2004 gardé pour mémoireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8792 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Ajout bug #1102herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8761 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-08Fix bug #931: leave dependent evars as such for refineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Erreur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6425 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Ajout bug #888herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Ajout bug #889herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6416 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-12Ajout exemple Yvesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5091 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Refine et let-infilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2012 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 07:23:57 +0000