| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-27 | Fix test for #3848, still open. | Maxime Dénès | |
| 2015-02-27 | Moving test for #3467 to closed after PMP's fix. | Maxime Dénès | |
| 2015-02-27 | Fix test-suite files for bugs #2456 and #3593, still open. | Maxime Dénès | |
| 2015-02-27 | Make coq_makefile generate double-colon rules for clean and archclean. (Fix ↵ | Guillaume Melquiond | |
| bug #4080) | |||
| 2015-02-27 | Somehow 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-27 | Add test-suite file for #3649. | Maxime Dénès | |
| 2015-02-27 | Moving tests for #2456 and #3593 to "opened" until they're fixed. | Maxime Dénès | |
| 2015-02-27 | Made test for #3392 rely less on unification. | Maxime Dénès | |
| 2015-02-27 | Moving test of #3848 to "opened". | Maxime Dénès | |
| 2015-02-26 | Test for #2602, which seems now fixed. | Maxime Dénès | |
| 2015-02-26 | Test for bug #3298. | Pierre-Marie Pédrot | |
| 2015-02-26 | Fixing bug #3298. | Pierre-Marie Pédrot | |
| 2015-02-26 | Trying to fix code locating camlp4/camlp5. | Maxime Dénès | |
| Should fix #3396 and #3964. | |||
| 2015-02-26 | Fixing bug 3099. | Pierre-Marie Pédrot | |
| 2015-02-26 | Fixing printing error in coq_makefile. | Pierre-Marie Pédrot | |
| 2015-02-26 | Fixing printing of ordinals. | Pierre-Marie Pédrot | |
| 2015-02-26 | Mention -R option in warnings, fixing #4067 and #4068. | Maxime Dénès | |
| 2015-02-26 | Fix checker after addition of a universe context in with t := c constraints. | Matthieu Sozeau | |
| 2015-02-26 | Fixing complexity tests for #4076. | Maxime Dénès | |
| 2015-02-26 | Revert "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-26 | Moving test for bug #3681 as closed. | Pierre-Marie Pédrot | |
| 2015-02-25 | CoqIDE: correclty unfocus (remove all tags) when jumping out of a proof | Enrico Tassi | |
| 2015-02-25 | STM: proof state also includes meta counters | Enrico Tassi | |
| Workers send back incomplete system states (only the proof part). Such part must include the meta/evar counter. | |||
| 2015-02-25 | Not 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-25 | Fix phony targets. (Fix for bug #4083) | Guillaume Melquiond | |
| 2015-02-25 | Reorder 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-25 | Another test for a variant of complexity problem #4076 (thanks to A. Mortberg). | Hugo Herbelin | |
| 2015-02-25 | Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integrating | Hugo Herbelin | |
| ensure_evar_independent into is_constrainable_in (a simpler approach closest to what existed before cf6a68b45). | |||
| 2015-02-25 | Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076). | Hugo Herbelin | |
| 2015-02-25 | An optimization on filtering evar instances with let-ins suggested by | Hugo 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-24 | Calling 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-24 | New 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. | |||
| 2015-02-24 | Refactoring in [Constr]. | Arnaud Spiwack | |
| [compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq]. | |||
| 2015-02-24 | [info_auto] & [info_trivial]: warning message to help users find [Info]. | Arnaud Spiwack | |
| 2015-02-24 | [info] tactical warning: do not suggest [info_auto] and [info_trivial]. | Arnaud Spiwack | |
| Since they don't work anymore. | |||
| 2015-02-24 | CHANGES: Info command + info_auto currently broken. | Arnaud Spiwack | |
| 2015-02-24 | Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a on | Hugo Herbelin | |
| integrating ensure_evar_independent into is_constrainable_in. | |||
| 2015-02-24 | Update the list of phony targets produced by coq_makefile. (Fix for bug #4084) | Guillaume Melquiond | |
| Also make uninstall_me.sh a real target with proper dependencies. | |||
| 2015-02-24 | Univs: Fix Check calling the kernel to retype in the wrong environment. | Matthieu Sozeau | |
| Fixes bug #4089. | |||
| 2015-02-23 | Compensating 6fd763431 on postponing subtyping evar-evar problems. | Hugo Herbelin | |
| Pushing pending problems had the side-effect of later solving them in the opposite order as they arrived, resulting on different complexity (see e.g. #4076). We now take care of pushing them in reverse order so that they are treated in the same order. | |||
| 2015-02-23 | Fixing cf6a68b45 on integrating ensure_evar_independent into ↵ | Hugo Herbelin | |
| is_constrainable_in. | |||
| 2015-02-23 | Fixed doc of fresh (was already outdated before fixing #3233). | Pierre Courtieu | |
| 2015-02-23 | Fixed 3233 (fresh does not work with a qualid). | Pierre Courtieu | |
| fresh now accepts a qualid, and behaves as if given the short name. Since fresh used to accept an id, supporting qualid is IMO not a new feature but just a fix. Hence the fix in v8.5. | |||
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond | |
| 2015-02-23 | Test for #3953 (subst in evar instances). | Hugo Herbelin | |
| 2015-02-23 | Fixing rewrite/subst when the subterm to rewrite is argument of an Evar. | Hugo Herbelin | |
| This was broken by the attempt to use the same algorithm for rewriting closed subterms than for rewriting subterms with evars: the algorithm to find subterms (w_unify_to_subterm) did not go through evars. But what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"? Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look in the instance? If we adopt the first approach, then, what to do when looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the instance? Is it normal that an evar behaves as a rigid constant when it cannot be unified with the pattern? | |||
| 2015-02-23 | Fixing occur-check which was too strong in unification.ml. | Hugo Herbelin | |
| 2015-02-23 | Fixing 934761875 about optimizing Import of several libraries at once ↵ | Hugo Herbelin | |
| (thanks to Enrico for noticing a bug). | |||
| 2015-02-23 | Fixing test #2830. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |