index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
complexity
Commit message (
Expand
)
Author
Age
*
Change Implicit Arguments to Arguments in test-suite
Jasper Hugunin
2018-03-30
*
An optimization of tactic constructor.
Hugo Herbelin
2017-09-19
*
Making parentheses mandatory in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
Fixing complexity file f_equal.v.
Hugo Herbelin
2015-11-06
*
Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan
Hugo Herbelin
2015-11-06
*
Fixing complexity tests for #4076.
Maxime Dénès
2015-02-26
*
Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).
Hugo Herbelin
2015-02-25
*
Compensating 6fd763431 on postponing subtyping evar-evar problems.
Hugo Herbelin
2015-02-23
*
Last test-suite not in Symmetric Patterns syntax
pboutill
2013-01-21
*
Minor fixes in the test-suite after my recent commits
letouzey
2012-07-06
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
remove undocumented and scarcely-used tactic auto decomp
letouzey
2012-04-23
*
Fixing format of complexity bug Notations.v.
herbelin
2011-12-17
*
Fixing amazing loop when using eta-expansion in pattern-matching for
herbelin
2011-12-16
*
Optimizing the compilation of unused aliases in pattern-matching.
herbelin
2011-11-21
*
Fixes in the test-suite after modularisation of ZArith and co
letouzey
2011-05-06
*
fixed guard check with commutative cuts
barras
2010-05-20
*
Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).
herbelin
2010-04-19
*
Small things about coqdoc + fixing lettuple.v test (part of bug #2289)
herbelin
2010-03-30
*
Fixing bug #2279 (printing nested let-in was in exponential time)
herbelin
2010-03-27
*
fixed minor pbs with test cases
barras
2010-03-12
*
introduced lazy computation of size info in the guard condition
barras
2010-03-11
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
illegal tactic application was having Ltac interpreter loop
barras
2009-03-04
*
commited complexity test for exponential behavior of unification
barras
2009-02-09
*
- Optimized "auto decomp" which had a (presumably) exponential in
herbelin
2008-12-26
*
test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq
letouzey
2008-07-09
*
Strategy commands are now exported
barras
2008-05-22
*
MAJ et bricoles diverses
herbelin
2008-05-12
*
Ajout d'un test de complexité de injection (cf bug 1173)
herbelin
2007-04-14
*
Pas de solution à court terme pour ce problème de complexité
herbelin
2007-01-28
*
Correction petits bugs du check de la test-suite
herbelin
2006-12-28
*
Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...
herbelin
2006-12-12
*
Test bug #932
herbelin
2006-12-12
*
Ajout test setoid_rewrite (cf bug #1176); anglicisation
herbelin
2006-11-01
*
Ajout d'un répertoire de test de la complexité
herbelin
2006-10-06