aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-03-02Now accepting unit props in mutual definitionsBruno Barras
2015-02-28Coq_makefile clean target erases .coq-native dirs in . if they are emptyPierre Boutillier
2015-02-28Fixing the rule for ml4 depencies in coq_makefilemlasson
2015-02-28Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ↵Pierre Boutillier
r15439 as we were talking at that time)
2015-02-27Adding a test for bug #3612.Pierre-Marie Pédrot
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-27Fixing OCaml 3.12 compilation.Pierre-Marie Pédrot
2015-02-27Test for bug #3249.Pierre-Marie Pédrot
2015-02-27Fixing bug #3249.Pierre-Marie Pédrot
Instead of substituting carelessly the recursive names in Ltac interpretation, we declare them in the environment beforehand, so that they get globalized as themselves. We restore the environment afterwards by transactifying the globalization procedure.
2015-02-27Taking current env and not global env in b286c9f4f42f (4 commits ago,Hugo Herbelin
as revealed by #2141).
2015-02-27simpl: honor Global for "simpl: never" (Close: 3206)Enrico Tassi
It was an integer overflow! All sorts of memories.
2015-02-27STM: Considering Stack_overflow as a normal tactic error (Close #3576)Enrico Tassi
2015-02-27Fix test for #3467, I had moved it in a dumb way.Maxime Dénès
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
2015-02-27Hack so that refine_no_check accepts an argument which is a match on anHugo Herbelin
inductive type with let-in in the arity (until logic.ml disappears).
2015-02-27Fixing first part of bug #3210 (inference of pattern-matching returnHugo Herbelin
clause in the presence of let-ins in the arity of inductive type).
2015-02-27Fixing typo resulting in wrong printing of return clauses forHugo Herbelin
inductive types with let-in in arity.
2015-02-27Fix test for #3848, still open.Maxime Dénès
2015-02-27Moving test for #3467 to closed after PMP's fix.Maxime Dénès
2015-02-27Fix test-suite files for bugs #2456 and #3593, still open.Maxime Dénès
2015-02-27Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵Guillaume Melquiond
bug #4080)
2015-02-27Somehow fixing bug #3467.Pierre-Marie Pédrot
The notations using tactics in term seem now not to respect globalized names. It is not obvious that this is the expected behaviour, but at least it does not die with an anomaly.
2015-02-27Add test-suite file for #3649.Maxime Dénès
2015-02-27Moving tests for #2456 and #3593 to "opened" until they're fixed.Maxime Dénès
2015-02-27Made test for #3392 rely less on unification.Maxime Dénès
2015-02-27Moving test of #3848 to "opened".Maxime Dénès
2015-02-26Test for #2602, which seems now fixed.Maxime Dénès
2015-02-26Test for bug #3298.Pierre-Marie Pédrot
2015-02-26Fixing bug #3298.Pierre-Marie Pédrot
2015-02-26Trying to fix code locating camlp4/camlp5.Maxime Dénès
Should fix #3396 and #3964.
2015-02-26Fixing bug 3099.Pierre-Marie Pédrot
2015-02-26Fixing printing error in coq_makefile.Pierre-Marie Pédrot
2015-02-26Fixing printing of ordinals.Pierre-Marie Pédrot
2015-02-26Mention -R option in warnings, fixing #4067 and #4068.Maxime Dénès
2015-02-26Fix checker after addition of a universe context in with t := c constraints.Matthieu Sozeau
2015-02-26Fixing complexity tests for #4076.Maxime Dénès
2015-02-26Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Maxime Dénès
This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035.
2015-02-26Moving test for bug #3681 as closed.Pierre-Marie Pédrot
2015-02-25CoqIDE: correclty unfocus (remove all tags) when jumping out of a proofEnrico Tassi
2015-02-25STM: proof state also includes meta countersEnrico Tassi
Workers send back incomplete system states (only the proof part). Such part must include the meta/evar counter.
2015-02-25Not building the doc by default.Maxime Dénès
Should make the compilation of Coq more robust against LaTeX errors. See e.g. #4091.
2015-02-25Fix phony targets. (Fix for bug #4083)Guillaume Melquiond
2015-02-25Reorder the steps of the easy tactic. (Fix for bug #2630)Guillaume Melquiond
Due to the way it was laid out, the tactic could prove neither (Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True) yet it could prove (Zle x x /\ True) and (P /\ Q |- P).
2015-02-25Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).Hugo Herbelin
2015-02-25Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integratingHugo Herbelin
ensure_evar_independent into is_constrainable_in (a simpler approach closest to what existed before cf6a68b45).
2015-02-25Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076).Hugo Herbelin
2015-02-25An optimization on filtering evar instances with let-ins suggested byHugo Herbelin
inefficiency #4076. In an evar context like this one x:X, y:=f(x), z:Z(x,y) |- ?x : T(x,y,z) with unification problem a:A, b:=f(t(a)) |- ?x[x:=t(a);y:=b;z:=u(a,b)] = v(a,b,c) we now keep y after filtering, iff the name b occurs effectively in v(a,b,c), while before, we kept it as soon as its expansion f(t(a)) had free variables in v(a,b,c), which was more often, but useless since the point in keeping a let-in in the instance is precisely to reuse the name of the let-in while unifying with a right-hand side which mentions this name.
2015-02-24Calling coq references lazily in plugin cc so as to support static linking ↵Hugo Herbelin
of plugins.
2015-02-24[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is ↵Arnaud Spiwack
progress. Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far. Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it). Fixes bugs (one reported directly on coqdev, and #3412).
2015-02-24New function [Constr.equal_with] to compare terms up to variants of ↵Arnaud Spiwack
[kind_of_term]. To be able to write equality up to evar instantiation instantiation. Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 01:16:39 +0000