| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-12-06 | Fix broken documentation in presence of \zeroone{... \tt ...}. | Guillaume Melquiond | |
| The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there. | |||
| 2016-12-06 | Update documentation (bugs #5246 and #5251). | Guillaume Melquiond | |
| 2016-11-08 | Merge remote-tracking branch 'github/pr/348' into v8.6 | Maxime Dénès | |
| Was PR#348: Credits for 8.6 | |||
| 2016-11-07 | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès | |
| Was PR#339: Documenting type class options, typeclasses eauto | |||
| 2016-11-07 | Document two new variants of refine | Matthieu Sozeau | |
| They allow to call refine without doing typeclass resolution, allowing to use refine in typeclass hints. | |||
| 2016-11-05 | Minor fix in documentation | Matthieu Sozeau | |
| 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 | 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-25 | Remove v62 from the refman. | Théo Zimmermann | |
| 2016-10-24 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-19 | Documenting Hint Resolve -> and <- variants. | Théo Zimmermann | |
| These variants are from 8.3 but were never documented except in CHANGES. | |||
| 2016-10-19 | Making the doc of auto hints more precise. | Théo Zimmermann | |
| The doc of auto hints now mention again that sometimes a hint will be used with simple apply and sometimes it will be used with exact. It does not try to be fully precise in that we don't necessarily want to document the behaviors of auto that we might like to change. See also the discussion on commit 9227d6e. | |||
| 2016-10-18 | Extending the doc with a general summary of auto variants. | Théo Zimmermann | |
| This way of giving the summary avoids redundancy as much as possible. It is helpful for the auto-completion of Company-Coq of @cpitclaudel. | |||
| 2016-10-18 | Document info_auto. | Théo Zimmermann | |
| Now that this tactic has been fixed (commit 58d1381), it needed to get documented. | |||
| 2016-10-18 | Improve the documentation of eauto. | Théo Zimmermann | |
| Improve the description of what auto/eauto do. These two tactics rely on the simple version of apply/eapply. Since this simple version is available to the end user, it is better to mention it. See also the confusion that such description can create in the thread "Understanding auto" on Coq-Club. | |||
| 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-09-30 | Merge branch 'v8.5' into v8.6 | Maxime Dénès | |
| 2016-09-28 | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès | |
| Was PR#232: Fix the parsing of goal selectors. | |||
| 2016-09-27 | Fixing #4887 (confusion between using and with in documentation of firstorder). | Hugo Herbelin | |
| 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-12 | Refolding: disable in 8.4 compat file, document | Matthieu Sozeau | |
| 2016-08-21 | Documenting "Set Structural Injection". | Hugo Herbelin | |
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès | |
| 2016-06-30 | Update the documentation for goal selectors. | Cyprien Mangin | |
| 2016-06-29 | Updated CHANGES about subst. More on recursive equations in reference manual. | Hugo Herbelin | |
| 2016-06-16 | Document new Hint Mode option. | Matthieu Sozeau | |
| 2016-06-16 | Revise syntax of Hint Cut | Matthieu Sozeau | |
| As noticed by C. Cohen it was confusingly different from standard notation. | |||
| 2016-06-14 | Add documentation for goal selectors. | Cyprien Mangin | |
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-05-03 | In Regular Subst Tactic mode, ensure that the order of hypotheses is | Hugo Herbelin | |
| preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual. | |||
| 2016-03-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-02-24 | Document Hint Mode, cleanup Hint doc. | Matthieu Sozeau | |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-20 | Clarifying the documentation of tactics "cbv" and "lazy". | Hugo Herbelin | |
| Following a discussion on coq-club on Jan 13, 2016. | |||
| 2016-01-14 | Updating and improving the documentation of intros patterns. | Hugo Herbelin | |
| In particular, documenting bracketing of last pattern on by default. | |||
| 2016-01-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-12 | Documenting dtauto and dintuition. | Hugo Herbelin | |
| 2016-01-12 | Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding". | Hugo Herbelin | |
| 2016-01-12 | Documenting option 'Set Bracketing Last Introduction Pattern'. | Hugo Herbelin | |
| 2016-01-12 | restore documentation of admit | Enrico Tassi | |
| 2015-12-17 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-16 | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable". | Guillaume Melquiond | |
| 2015-12-15 | Simplifying documentation of "assert form as pat". | Hugo Herbelin | |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-10 | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | |
| Marking it as experimental. | |||
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond | |
| 2015-12-05 | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) | Hugo Herbelin | |
| based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. | |||
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |