aboutsummaryrefslogtreecommitdiff
path: root/test-suite/complexity
AgeCommit message (Collapse)Author
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
2009-03-04illegal tactic application was having Ltac interpreter loopbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11963 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-09commited complexity test for exponential behavior of unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11894 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-26- Optimized "auto decomp" which had a (presumably) exponential inherbelin
the number of conjunctions to split. - A few cleaning and uniformisation in auto.ml. - Removal of v62 hints already in core. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-09test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eqletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11216 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22Strategy commands are now exportedbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-12MAJ et bricoles diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10923 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-14Ajout d'un test de complexité de injection (cf bug 1173)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9769 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-28Pas de solution à court terme pour ce problème de complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9548 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-28Correction petits bugs du check de la test-suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Backtrack sur suppression des vars anonymes des contextes d'evars (echec ↵herbelin
Case15.v et CasesDep.v pas anormal) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9437 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-12Test bug #932herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9434 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-01Ajout test setoid_rewrite (cf bug #1176); anglicisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9330 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Ajout d'un répertoire de test de la complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9222 85f007b7-540e-0410-9357-904b9bb8a0f7