aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
...
* Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weGravatar herbelin2010-09-19
| | | | | | revert the catch of anomalies in reductionops.ml now (commit 13353)? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inGravatar herbelin2010-09-18
| | | | | | coqdep since it is now deterministic (later -R's overwriting former ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
| | | | | | | | | | | | | | | | | too late, in a global environment which was no longer the correct one, leading to the failure of error printing (hence an anomaly) in case the command modified the state in several steps. Now, errors raised by vernac commands are processed in the same (intermediate) state they were raised from, just before rolling back to the original state. that modify the state in several Now, errors raised by vernac commands that modify the state in several steps (say S1, S2, ..., Sn) are processed in the state they were produced in (S1, S2, ... Sn-1), git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
| | | | | | | | | | both for interpreting ltac patterns and patterns of "change pat with term". In particular, in the current status, Goal evars needs mandatorily to have the hole_kind GoalEvar. If this is too complicated to enforce, we might eventually consider another approach to the question of interpreting patterns in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13428 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
| | | | | | | | | | | | | | user either gives all missing arguments not dependent in the concl or all missing arguments not *recursively* dependent in the concl (as introduced by commit 13367). In practice, this means that "apply f_equal with A" remains allowed even though the new, recursive, analysis detects that all arguments of f_equal are inferable, including the first type argument (which is inferable from the knowledge of the function). Sized the opportunity to better explain the behavior of clenv_dependent. Also made minor code simplification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
| | | | | | | | | | - improving error message when a reference to unfold is not found - repairing anomaly when an evaluable reference exists at internalisation-time but not at run time, and similarly for an arbitrary term (but the latter is new from 8.3 because of the new use of retyping instead of understand for typing Ltac values) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13408 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2375 (congruence)Gravatar corbinea2010-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated test on Nsatz after Loïc moved NsatzR to Nsatz.Gravatar herbelin2010-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13361 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-case for bug #2105Gravatar barras2010-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13352 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesGravatar barras2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13337 85f007b7-540e-0410-9357-904b9bb8a0f7
* nstaz pour les anneaux integres et les setoides, R Z et QGravatar pottier2010-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
| | | | | | | | | | | | | - Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting fix to bug #2353 (fixpoint with recursively non-uniformGravatar herbelin2010-07-21
| | | | | | parameters) to branch 8.2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation and test-suite of nsatzGravatar glondu2010-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13279 85f007b7-540e-0410-9357-904b9bb8a0f7
* nsatz in an integral domain with specialization to Z and RGravatar pottier2010-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
| | | | | | | | | | | | them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.Gravatar herbelin2010-06-26
| | | | | | Fixing tests 2145.v about Nsatz. Adding nsatz target in Makefile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13203 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restored a "feature" of unification in pre-8.3 (it was used e.g. in aGravatar herbelin2010-06-25
| | | | | | | | | | | 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
* Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)Gravatar letouzey2010-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13172 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).Gravatar herbelin2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
* add in test-suite the scripts about fsetdec bugsGravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13165 85f007b7-540e-0410-9357-904b9bb8a0f7
* test for bug #2141 (include + extraction)Gravatar letouzey2010-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13160 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
| | | | | | | 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
* Fixing bug 2295 (omission of option "as" in return clause of "match" was notGravatar herbelin2010-06-13
| | | | | | working with section/goal variables). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).Gravatar herbelin2010-06-13
| | | | | | | | 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
* Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withGravatar herbelin2010-06-13
| | | | | | | | 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
* Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"Gravatar herbelin2010-06-13
| | | | | | | | | | | | 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
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
| | | | | | enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
| | | | | | | | | | | - 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
* Added regression tests for bugs + miscellaneous improvementsGravatar herbelin2010-06-12
| | | | | | | | | - #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
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
| | | | | | | | | | | | | | | | 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
* Fixed bug # 2303 in r 13087.Gravatar msozeau2010-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
| | | | | | | | 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
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
| | | | | | | | | | 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
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
| | | | | | | 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
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - 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
* Backported r13068 to branch v8.3 (whd_betaiota on inferred returnGravatar herbelin2010-06-04
| | | | | | 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
* Grobner.v removedGravatar pottier2010-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13069 85f007b7-540e-0410-9357-904b9bb8a0f7
* plugin groebner updated and renamed as nsatz; first version of the doc of ↵Gravatar pottier2010-06-03
| | | | | | nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix xml test in non-local modeGravatar glondu2010-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix test-suite cleaningGravatar glondu2010-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
| | | | | | 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
* A little bit of cleanup, and some annotations.Gravatar fkirchne2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added examples for checking that the guard condition excludes subtermsGravatar herbelin2010-05-20
| | | | | | in impredicative types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug 2307Gravatar pboutill2010-05-20
| | | | | | | 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
* fixed guard check with commutative cutsGravatar barras2010-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13022 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 02:25:23 +0000