| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 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 | 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.6' | Pierre-Marie Pédrot | |
| 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 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 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-08 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 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 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 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.6' | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |