aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2013-03-18Fix for bug #3004 (thanks Hugo!)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16317 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵pboutill
fixpoint definition + Help the use of #trace on evar_conv_appr_x git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21A slightly more efficient test of well-typedness of restriction ofherbelin
evars (though this might be slighty more costly). This incidentally solves Appel's part of bug #2830 even though a conceptual problem around the interaction of unification with the proof engine has to be solved. Indeed, what to do when unification, called as part of a tactic, solves or refines the current goal by side effect. Somehow, unifyTerms or tclEVARS should take this possibility into consideration, either by forbidding the refinement of the current goal by side effect, or by acknowledging this refinement by producing new subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16232 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
interleaving of ltac and ml code is not visible (this particularly applies to ltac notation ring, which calls ml-level ring_lookup and Ring again at the ltac level, resulting in non-localisation of "ring" errors). Added also missing LtacLocated checks in Class_instance and Proofview. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
variable names). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16185 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16181 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29Added a file for testing regression of bug #2955 (anomaly in simpl inherbelin
the presence of aliased modules). Bug was actually fixed in trunk (thanks to PMP's monomorphization (and change of semantics) of equality over evaluable references. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16180 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-29Fixing bug #2969 (admit failing after Grab Existential Variables dueherbelin
to inconsistency in using evar_hyps which is unfiltered and evar_env which is filtered). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16175 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Fixed bug #2966 (de Bruijn error in computation of heads for coercions).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16168 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Fixing one part of #2830 (anomaly "defined twice" due to nested calls toherbelin
the function solve_candidates introduced in 8.4). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16163 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7
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
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
(e.g. 1 for eq_refl). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Taking into account the possibility of having a type of type which isherbelin
an evar in typing.ml. Thanks to HoTT people for noticing the problem. Fixed behavior of e_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16092 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
different instances of a meta are checked against full conversion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16086 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
IT happens that there are some other uses of casts, e.g. in nat_int de MathClasses which uses a notation 0 for some class constructor zero, and a cast (0:nat) to force this notation 0 to represent the instance O in nat of the class of types having a zero (eventually, 0, i.e. "zero nat O" and "O" are convertible but the information of being a class instance is lost). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
notations: - hopefully never 2 spaces when the user did not ask for - more systematic default insertion of spaces around symbols - e.g. have space before "[" if after a non-terminal - have spaces between consecutive terminals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16019 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-28Evarconv: Fix #2936 + commentspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16011 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
check condition in pattern-unification, resulting in the instantiation of evars by terms depending on themselves, henceforth leading eventually to a stack overflow. Occur-check in the arguments of evars was also missing. [Also fixed what looked like a typo in the env passed to project_evar_on_evar on line 1611.] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15996 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-21Fixing test-suite: Scope.vppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15990 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-18Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)herbelin
universes. As it uses eq_rect on Type(2), the arguments of eq_rect has to be in Type(3) and compiling the standard library now needs one more universe! If needed, we could avoid this by inlining the definition of (eq_rect Type2) in Hurkens.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15981 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Update output/Search.out after hint-related extra defs in Peanoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15980 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
type in "cast" to activate the temporary interpretation scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Fix test-suite output/* in benchpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15906 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04test-suite: fix grep rule for output testspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15770 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-04test-suite uses coqtop instead of coqtop.bytepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15769 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24In the output tests, ignore dynlink messagesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15767 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
We now always produce two binaries, coqtop and coqtop.byte : - If ocamlopt is available, coqtop is directly what used to be coqtop.opt, no more symlinks needed. - Otherwise, coqtop is a copy of coqtop.byte. The same for coqchk and coqide... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
It uses a term in front of a stack instead of a term in front of a list of applied terms. From outside of eq_appr_x nothing should have changed. Nasty evar instantiation bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-29Fixing #2836 (materialize_evar might refine as a side effect theherbelin
current evar to project; this may happen if this evar is dependent and is involved in evar-evar conversion problem eventually solved by instantiating the current evar; could maybe be optimized when the evar to materialize has invertible instance in which case define_evar_from_virtual_equation applied on the current evar could be shortcut, avoiding to create an evar). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-21Fixing bug #2835 (the rationale for printing notations was notherbelin
standard under lambdas and products). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15644 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-21Improving management of notations with binders (see #2708 where aherbelin
variable is used both as term and as binder, resulting in ununderstandable error message about scopes). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15642 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Restore test file induct.v where the "in |- *" is mandatoryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15585 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-06Continuing r15459: it helps testing occur-check early in someherbelin
situations (see rewrite MonoidMonadTrans.bind_toLower' in Misc/QuicksortComplexity/monoid_expec.v). Also fixing badly designed test 2817.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15543 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-05Legacy Ring and Legacy Field migrated to contribsletouzey
One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 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-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
known instances in unification.ml). This refines the fix to bug #1918. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-20Fixing bug #2809 (anomaly when printing a module with notations due toherbelin
bad interaction between lazy evaluation of pp streams and temporary effectful extension of global environment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15457 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-18Proof using: nested sections bugfixgareuselesinge
It used to be the case that the list of declared section variables for a constant was taken into account only when discharging the first enclosing sections, but not any outer section. Example of the bug: Section A. Variable x : bool. Section B. Variable y : nat. Lemma foo : True. Proof using x y. Admitted. End B. End A. Check foo. (* nat -> True instead of bool -> nat -> True *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15445 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-14Constrextern is allow to use partially applied notationspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15440 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12Fixing test-suite after last storm in Pp.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:19:19 +0000