| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-11-07 | Merge commit 'e6edb33' into v8.6 | Maxime Dénès | |
| Was PR#331: Solve_constraints and Set Use Unification Heuristics | |||
| 2016-11-07 | More explicit name for status of unification constraints. | Maxime Dénès | |
| 2016-11-05 | More precise refine compatibility | Matthieu Sozeau | |
| 2016-11-04 | Fix #3441 Use pf_get_type_of to avoid blowup | Matthieu Sozeau | |
| ... in pose proof of large proof terms | |||
| 2016-11-04 | Fix refine in compatibility mode | Matthieu Sozeau | |
| 2016-11-04 | Merge remote-tracking branch 'github/pr/335' into v8.6 | Maxime Dénès | |
| Was PR#335: Fix printing of typeclasses eauto debug wrt intro. | |||
| 2016-11-04 | Merge remote-tracking branch 'github/pr/336' into v8.6 | Maxime Dénès | |
| Was PR#336: Remove v62 | |||
| 2016-10-28 | Merge remote-tracking branch 'github/pr/321' into v8.6 | Maxime Dénès | |
| Was PR#321: Handling of section variables in hints | |||
| 2016-10-26 | Using msg_info for info_auto and info_eauto (PR #324). | Hugo Herbelin | |
| 2016-10-26 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-25 | Merge remote-tracking branch 'github/pr/338' into v8.5 | Maxime Dénès | |
| Was PR#338: Remove warning now that info_auto is fixed. | |||
| 2016-10-25 | Remove warning now that info_auto is fixed. | Théo Zimmermann | |
| Removes a warning dating from 8.5 signaling that info_auto and info_trivial are broken and advising to use Info 1 auto instead. Now, these tactics are fixed and thus they can be used again. They do not do exactly the same thing as Info 1 auto and may be more useful for the learner. | |||
| 2016-10-25 | Remove v62 from the codebase. | Théo Zimmermann | |
| 2016-10-25 | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | |
| This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses. | |||
| 2016-10-24 | Fix printing of typeclasses eauto debug wrt intro. | Théo Zimmermann | |
| 2016-10-22 | Fixing printing of generic arguments of tag "var". | Hugo Herbelin | |
| 2016-10-22 | Renamings to avoid confusion deprecating old names | Matthieu Sozeau | |
| reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics | |||
| 2016-10-21 | sections/hints: prevent Not_found in get_type_of | Matthieu Sozeau | |
| due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared. | |||
| 2016-10-17 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-15 | Still a problem with debug auto printing. | Hugo Herbelin | |
| "msg_debug (mt())" is not identity, so we return back to how it was done in 8.4, contracting a repeated pattern-matching into one. | |||
| 2016-10-15 | One more little bug in the output of "debug auto". | Hugo Herbelin | |
| Header was missing in last commit. One day, it would be nice to unify the display of "debug auto" and "debug eauto"... | |||
| 2016-10-14 | Fix bug #5139: Anomalies should not be caught by || / try. | Pierre-Marie Pédrot | |
| There was a catch-all clause in the tclORELSE0 function. We now only catch noncritical exceptions. | |||
| 2016-10-14 | Fixing printing of info_auto broken since 0091c528 (2014). | Hugo Herbelin | |
| 2016-10-14 | Fixing English typography for colon. | Hugo Herbelin | |
| 2016-10-14 | Using "simple apply" and "simple eapply" in the trace of auto. | Hugo Herbelin | |
| This is more precise and probably clearer (see e.g. thread "Understanding auto" on coq-club). | |||
| 2016-10-12 | Fix bug #4958: [debug auto] should specify hint databases. | Pierre-Marie Pédrot | |
| 2016-10-10 | Fix #4416: - Incorrect "Error: Incorrect number of goals" | Arnaud Spiwack | |
| In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416). | |||
| 2016-10-07 | Fix bug #4464: "Anomaly: variable H' unbound. Please report.". | Pierre-Marie Pédrot | |
| We simply catch the RetypeError raised by the retyping function and translate it into a user error, so that it is captured by the tactic monad instead of reaching toplevel. | |||
| 2016-10-05 | Clean up type classes flags and update compat file. | Maxime Dénès | |
| 2016-10-03 | Merge remote-tracking branch 'github/pr/263' into v8.6 | Maxime Dénès | |
| Was PR#263: Fast lookup in named contexts | |||
| 2016-10-03 | fixing bug 4609: document an option governing the generation of equalities | Yves Bertot | |
| between proofs in tactic injection, with a side-effect on inversion. | |||
| 2016-10-02 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-01 | Micro refactoring: use exact_no_check. | Théo Zimmermann | |
| This does not affect the semantics of these functions. | |||
| 2016-09-30 | Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime. | Hugo Herbelin | |
| 2016-09-30 | Fix bug #5045: [generalize] creates ill-typed terms in 8.6. | Pierre-Marie Pédrot | |
| 2016-09-30 | Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk. | Pierre-Marie Pédrot | |
| This bug was introduced by 37ab45726, because the new apply_type function was not checking that the new goal was indeed well-typed. We add this check locally in the generalize dependent tactic. | |||
| 2016-09-30 | Merge branch 'v8.5' into v8.6 | Maxime Dénès | |
| 2016-09-30 | Merge branch '4762' into v8.5 | Maxime Dénès | |
| Was PR#293: Fix #4762 (eauto weaker than auto). | |||
| 2016-09-30 | Fix #4762. | Cyprien Mangin | |
| 2016-09-29 | Fix a bug in subst releaved by an OCaml warning. | Maxime Dénès | |
| 2016-09-27 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-24 | Moving "move" in the new proof engine. | Hugo Herbelin | |
| 2016-09-24 | Ensuring that the evar name is preserved by "rename" as it is already | Hugo Herbelin | |
| the case for clear and the conversion tactics. | |||
| 2016-09-16 | Addressing OCaml compilation warnings. | Hugo Herbelin | |
| One of them revealed a true bug. | |||
| 2016-09-15 | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵ | Hugo Herbelin | |
| ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5. | |||
| 2016-09-15 | Typo. | Hugo Herbelin | |
| 2016-09-09 | Tracking careless uses of slow name lookup. | Pierre-Marie Pédrot | |
| 2016-09-04 | Do not normalize evars in Eauto.e_give_exact. | Pierre-Marie Pédrot | |
| This is not needed, as the terms are then checked up to unification or convertibility. | |||
| 2016-09-02 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-01 | Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior). | Hugo Herbelin | |
| (It was reducing also in hypotheses.) | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |