aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-03-03Reinstalling search of camlpX in camldir, when given, forHugo Herbelin
compatibility with pre-1b7d4a033af heuristic in searching camlpX (continuation of a joint patch with Maxime). Typo basename -> dirname.
2015-03-03Typos in doc modules.Hugo Herbelin
2015-03-03Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeMatthieu Sozeau
cases, in some cases.
2015-03-03Fix bug #4101, noccur_evar's expand_projection can legitimately failMatthieu Sozeau
when called from w_unify, so we protect it.
2015-03-03Fix bug introduced by my last commit, forgetting to adjust de BruijnMatthieu Sozeau
index lookup.
2015-03-02Fix bug #4097.Matthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:31:41 +0000