aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/refine.v
AgeCommit message (Expand)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
2017-08-21Fixing another regression with 8.4 wrt to βι-normalization of created hyps.Hugo Herbelin
2015-12-15Fix test-suite files after change in refine tactic.Maxime Dénès
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-01-18Unset Asymmetric Patternspboutill
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-11-04Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)herbelin
2007-05-18Wish #1582 (3eme)herbelin
2006-11-10Correction d'un bug refineherbelin
2006-05-05Vieux bug de fin 2004 gardé pour mémoireherbelin
2006-04-28Ajout bug #1102herbelin
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2005-03-08Fix bug #931: leave dependent evars as such for refineherbelin
2004-12-06Erreur commit précédentherbelin
2004-12-06Ajout bug #888herbelin
2004-12-06Ajout bug #889herbelin
2003-12-12Ajout exemple Yvesherbelin
2001-09-20Refine et let-infilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:37:17 +0000