aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/setoid_test.v
Commit message (Expand)AuthorAge
* An example which failed in 8.5 and that d670c6b6 fixes.Gravatar Hugo Herbelin2016-04-07
* Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-03-28
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...Gravatar msozeau2013-06-10
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
* Fix test-suite script.Gravatar msozeau2011-02-21
* Correct handling of existential variables when multiple differentGravatar msozeau2011-02-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Uniformisation of some error messages + added test on setoid rewrite.Gravatar herbelin2009-01-07
* Fix setoid tests, use red for a Setoid_Theory lemma, and ParametricGravatar msozeau2008-04-14
* New implementation of Add Relation as a DefaultRelation instanceGravatar msozeau2008-03-08
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Test de non-régression pour commit 9673Gravatar herbelin2007-03-15
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* * setoid_test.v removed and added again in new syntaxGravatar sacerdot2004-09-03
* ajout d'un fichier test pour setoidesGravatar clrenard2001-09-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 19:12:05 +0000