| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-11-07 | Fixes to compile with ocaml 4.01 | Matthieu Sozeau | |
| 2016-11-03 | Rework search_strategy option handling | Matthieu Sozeau | |
| 2016-11-03 | Internal API change to typeclasses eauto. | Théo Zimmermann | |
| This commit makes the traversing strategy of typeclasses eauto an optional argument of the function that implements it. This change should be non-breaking. | |||
| 2016-11-03 | Do not shelve non-class subgoals but fail, it should | Matthieu Sozeau | |
| be the instance writer's responsibility to not generated non-dependent non-class subgoals (otherwise we loose compatibility as shown in e.g. MathClasses, which goes into loops because of unexpectedly unconstrained goals). Reflect it in the doc. | |||
| 2016-11-03 | typeclasses eauto Implem/doc of shelving strategy | Matthieu Sozeau | |
| Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented. | |||
| 2016-11-03 | Fix [typeclasses eauto with] and nopattern hints | Matthieu Sozeau | |
| This was the source of a bug in #5115#c7. | |||
| 2016-11-03 | Fix handling of only_classes at toplevel | Matthieu Sozeau | |
| 2016-11-03 | Handle Unique Solutions flag. | Matthieu Sozeau | |
| 2016-11-03 | TCS: error handling and debug printing in resolution | Matthieu Sozeau | |
| 2016-11-03 | Fix bugs in Filtered Unification and cleanup code | Matthieu Sozeau | |
| 2016-11-03 | Fix Typeclasses eauto := bfs. | Matthieu Sozeau | |
| 2016-11-03 | Lets Hints/Instances take an optional pattern | Matthieu Sozeau | |
| In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well. | |||
| 2016-10-29 | Documenting changes in typeclasses | Matthieu Sozeau | |
| 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 | 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-22 | Fixing printing of generic arguments of tag "var". | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |