aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity
Commit message (Expand)AuthorAge
* An optimization of tactic constructor.Gravatar Hugo Herbelin2017-09-19
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Fixing complexity file f_equal.v.Gravatar Hugo Herbelin2015-11-06
* Fixing complexity issue with f_equal. Thanks to J.-H. JourdanGravatar Hugo Herbelin2015-11-06
* Fixing complexity tests for #4076.Gravatar Maxime Dénès2015-02-26
* Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).Gravatar Hugo Herbelin2015-02-25
* Compensating 6fd763431 on postponing subtyping evar-evar problems.Gravatar Hugo Herbelin2015-02-23
* Last test-suite not in Symmetric Patterns syntaxGravatar pboutill2013-01-21
* Minor fixes in the test-suite after my recent commitsGravatar letouzey2012-07-06
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
* Fixing format of complexity bug Notations.v.Gravatar herbelin2011-12-17
* Fixing amazing loop when using eta-expansion in pattern-matching forGravatar herbelin2011-12-16
* Optimizing the compilation of unused aliases in pattern-matching.Gravatar herbelin2011-11-21
* Fixes in the test-suite after modularisation of ZArith and coGravatar letouzey2011-05-06
* fixed guard check with commutative cutsGravatar barras2010-05-20
* Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).Gravatar herbelin2010-04-19
* Small things about coqdoc + fixing lettuple.v test (part of bug #2289)Gravatar herbelin2010-03-30
* Fixing bug #2279 (printing nested let-in was in exponential time)Gravatar herbelin2010-03-27
* fixed minor pbs with test casesGravatar barras2010-03-12
* introduced lazy computation of size info in the guard conditionGravatar barras2010-03-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* commited complexity test for exponential behavior of unificationGravatar barras2009-02-09
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eqGravatar letouzey2008-07-09
* Strategy commands are now exportedGravatar barras2008-05-22
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* Ajout d'un test de complexité de injection (cf bug 1173)Gravatar herbelin2007-04-14
* Pas de solution à court terme pour ce problème de complexitéGravatar herbelin2007-01-28
* Correction petits bugs du check de la test-suiteGravatar herbelin2006-12-28
* Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...Gravatar herbelin2006-12-12
* Test bug #932Gravatar herbelin2006-12-12
* Ajout test setoid_rewrite (cf bug #1176); anglicisationGravatar herbelin2006-11-01
* Ajout d'un répertoire de test de la complexitéGravatar herbelin2006-10-06