aboutsummaryrefslogtreecommitdiff
path: root/test-suite/complexity
AgeCommit message (Collapse)Author
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20fixed guard check with commutative cutsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13022 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-19Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).herbelin
Reasoning modulo variable aliases induced an extra lookup in the environment at each inversion of the components of the evar instances: precomputing the aliases map allowed to gain a factor n. Moreover, solve_evar_evar_l2r was recomputing the evar substitution from the evar instance n more times than needed. Function solve_evar_evar_l2r is still on O(n^2) but it does not seem to be used so often actually. The trivial case has been optimized (linear time) but the general case could probably be also cut down to O(n*log(n)) if needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12954 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
In coqdoc, made links to utf8 notations working and made representation of locations for notations more compact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-27Fixing bug #2279 (printing nested let-in was in exponential time)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12887 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-12fixed minor pbs with test casesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12865 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-11introduced lazy computation of size info in the guard conditionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12862 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 02:34:35 +0000