aboutsummaryrefslogtreecommitdiff
path: root/test-suite/complexity
AgeCommit message (Collapse)Author
2020-11-18[micromega] Updated test-suiteBESSON Frederic
Moved bug_13227.v to complexity/bug_13227_i.v
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-04-30Replace QSeqEquiv by QCauchySeq, simplify proofs.Vincent Semeria
Force Cauchy modulus equal to identity, make division transparent Fix test
2020-04-26constructive square rootVincent Semeria
Convert into a performance test Put time bound at the beginning of file Add Time command in the test
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2019-11-28Relax the pattern complexity testJason Gross
c.f. discussion at https://github.com/coq/coq/pull/11177#issuecomment-559139477
2019-11-26Update test-suite/complexity/pattern.vJason Gross
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2019-11-25Add a complexity test for `pattern`Jason Gross
This is to hopefully prevent regressions on https://github.com/coq/coq/issues/11150 and https://github.com/coq/coq/issues/6502.
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2017-09-19An optimization of tactic constructor.Hugo Herbelin
As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time.
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2015-11-06Fixing complexity file f_equal.v.Hugo Herbelin
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
for reporting it. A "cut" was not appropriately chained on the second goal but on both goals, with the chaining on the first goal introducing noise.
2015-02-26Fixing complexity tests for #4076.Maxime Dénès
2015-02-25Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).Hugo Herbelin
2015-02-23Compensating 6fd763431 on postponing subtyping evar-evar problems.Hugo Herbelin
Pushing pending problems had the side-effect of later solving them in the opposite order as they arrived, resulting on different complexity (see e.g. #4076). We now take care of pushing them in reverse order so that they are treated in the same order.
2013-01-21Last test-suite not in Symmetric Patterns syntaxpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16132 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Minor fixes in the test-suite after my recent commitsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Fixing format of complexity bug Notations.v.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14800 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Fixing amazing loop when using eta-expansion in pattern-matching forherbelin
printing notations. Since notation printing is not typed, printing "F G" using a notation for "f (fun x => g)" recursively eta-expands G, then x, then a new x and so on forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14705 85f007b7-540e-0410-9357-904b9bb8a0f7
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-01-31 11:37:43 +0000