aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify" accepted evars as ordinary variables. I hope I did not invalidate some features that would have needed restricting conversion on evar-free terms, but since failure of conversion in presence of evars is redirected to the main unification algorithm, I guess it is OK. For better readibility, I also inlined and cleaned a bit trivial_unify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13193 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13172 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13165 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-16test for bug #2141 (include + extraction)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13160 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
Note that the code is no longer in constrextern.ml but in topconstr.ml where the code for reversing notations of term already was. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixing bug 2295 (omission of option "as" in return clause of "match" was notherbelin
working with section/goal variables). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13131 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).herbelin
By the way, there is an open problem of which conversion to use (conv, evarconv, with or w/o universes levels) when trying to unify multiple instances of the same variable in ltac pattern-matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13130 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withherbelin
metas in return predicate of "match"); propagated protection for #2310 ("refine" problem with dependent metas of higher-order type) in v8.3 to v8.2. Everything goes well in trunk thanks for the new proof engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13129 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
by a regular error in v8.3. Example behaves better in trunk thanks to new proof engine. In fact, there are two distinct solutions to a unification problem: should "refine" commit to one of them or leave the problem open? For trunk, improved the unification error message by enforcing nf_evar (but at some time, nf_evar in error messages should move to himsg because it is costly when errors are used for backtracking). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
- made the example work (a call to whd_meta was missing) - replaced the internal error messages of w_unify_to_subterm_list into user-understandable messages - incidentally fixed the meaning of whd_meta (which now takes an evd) and meta_name (which now does what it means and do not treat differently the instantiated metas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
- #2095 (not fixed in v8.2 but fixed in v8.3 and trunk) - #2108 (fixed in v8.2, v8.3, trunk) - #2102 (moved warning to msg_warning to ensure flushing, but still open enhancement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13121 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
Use two ways to solve it: - added a whd_betaiota in solve_simple_eqn (since evarconv itself refuses beta to preserve the opportunities of first-order-matching expressions of the form "(fun x => P) t"; an advantage of this whd_betaiota is also that it may simplify K-redexes. - also added a last-chance test in case of failing occur-check by trying to fully head-normalize (with delta) the right-hand-side (allows to solve for instance "?n = id ?n" where id is a constant (a bridled form of solve_refl that use fconv instead of evar_conv_x). Incidentally improved a bit the rendering of the type of generalized terms in pattern-matching by using whd_betaiota. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13113 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fixed bug # 2303 in r 13087.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13104 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
products as implicit if they're part of a term and not a type (issue a warning instead). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
Definition's is not so painless. It seems to however generally provide "nicer" scripts so let us keep it and update the contribs and test-suite accordingly. Also enforced that the actual introduced names to be exactly as given in the statements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
Also updated perf-analysis file (the part of the commit that delays typing of ltac instances seems to slightly improve a few contributions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13096 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
- Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-04Backported r13068 to branch v8.3 (whd_betaiota on inferred returnherbelin
match predicate) and fixed Notation.out test accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13071 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-04Grobner.v removedpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13069 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of ↵pottier
nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Fix xml test in non-local modeglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13055 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Fix test-suite cleaningglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13052 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-28A little bit of cleanup, and some annotations.fkirchne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13036 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20Added examples for checking that the guard condition excludes subtermsherbelin
in impredicative types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13024 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20Fix bug 2307pboutill
Evars of source "ImpossibleCase" that remain undefined at the end of case analysis are now defined to ID (forall A : Type, A -> A). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13023 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-05-10Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13009 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-26Disable ideal-features tests by defaultglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12963 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-20Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)herbelin
+ changed printing of universe Type(0) to Set, so not to show that the implementation starts numbering with Set=Type(0) while documentation uses Type(0) for the common type of Prop and Set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12956 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-20Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2herbelin
(the bug was fixed for trunk/8.3 in revision 12354). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12955 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-04-18Fixed some printing bugs.herbelin
- Notations with coercions to funclass inserted were not working any longer since r11886. Made a fix but maybe should we eventually type the notations so that they have a canonical form (and in particular with coercions pre-inserted?). - Improved spacing management in printing extra tactic arguments "by" and "in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12951 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-17Moved Case3.v from ideal features to success (it works since 8.2).herbelin
Two other tests are still "ideal features" though not failing (evars_subst.v is a complexity test still of bad complexity and universes.v just describes an improvement to do without checking anything). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12949 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-13Remove only *.v.log files in clean of test-suite/Makefileglondu
...so that "./check > check.log" works as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12933 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12927 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Prettier test-suite/Makefileglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12925 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
numerals are open (see e.g. part of bug report #2044). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12924 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Use the Makefile in test-suite/checkglondu
The output format is preserved, but not the dynamics (results are showed all at once at the end). This script could be removed altogether once the main Makefile (and daily bench) are fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12922 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Makefile for the test-suiteglondu
Using a Makefile for tests allows (easily) running them in parallel, running and/or benching a single one, adding depedencies between them, and running them with a version of Coq different than the one compiled with the current source tree. The new way to make statistics about successes/failures is also more reliable (I found bugs in the previous one). Statistics (on AMD Phenom(tm) 9950 Quad-Core Processor 2.6 GHz): - plain sh script: ~ 3 min - make -j6: ~ 1 min git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12921 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Fix typos in test-suite scriptglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12920 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Test for bug #2231 (unexpected error when using let/if over an inductiveherbelin
parameter in the type of a constructor). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12918 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-07Commit 12906 continued (forgotten file).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12907 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-07Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichherbelin
was actually failing for another reason than the reason originally filled in the bug tracker) and revealed a bug in the unification.v test file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12906 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-06New model for user-driven translation of tokens in coqdocherbelin
In the initial model (formerly to r11432), coqdoc parsed separatedly letters and symbolic characters and was thus not able to translate tokens mixing letters and symbolic characters such as "\in" or "=_h". Revision 11432 extended the definition of translatable tokens by supporting letters in it with the benefit of supporting "\in" or "=_h" but added the constraint of requiring spaces to correctly separate tokens in expressions such as "x : nat" which otherwise would be split into "x" and ":nat", then leading to fail understanding "nat" as a proper reference. The new model renounces to define a lexical category of tokens and uses instead a dynamically extensible sublexer similar to the one used in the Coq lexer. The new model works even if tokens are not separated by spaces in the source file and it thus solves problems such as the one mentioned in bug #2273 (failure to link C in "`(!C)"). However, it imposes a stronger discipline in writing the lexing rules in cpretty.mll because the characters that can eventually contribute to the application of a printing rule are buffered in the sublexer and no output is allowed to occur until the buffer of the sublexer if flushed. The theoretical overhead due to the intermediate use of buffers is apparently less than 5%. More details on the token cutting discipline can be found in the new file token.mli. Incidentally fixed two small problems with notation links in LaTeX: made escaping of characters in LaTeX labels more robust so that notations do not easily get the same label name; avoid only highlighting the first '"' of a notation def (failing to have now a better highlighting strategy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12905 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Granting wish #2251 (forbidding rewriting a term reduced to an evar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12900 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Tests for bug report #2244 (pattern-unification with abstraction over Meta's)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12899 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 13:52:16 +0000