| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-12-26 | 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-26 | Update documentation (bugs #5246 and #5251). | Guillaume Melquiond | |
| 2016-12-26 | Fix some documentation typos. | Guillaume Melquiond | |
| 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-09-27 | Fixing #4887 (confusion between using and with in documentation of firstorder). | Hugo Herbelin | |
| 2016-09-19 | Replace { command ; } with ( command ) | Erik Martin-Dorel | |
| as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output. | |||
| 2016-09-19 | Fix typos in RefMan-uti.tex. | Erik Martin-Dorel | |
| - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace. | |||
| 2016-08-04 | Fix documentation typo (bug #4994). | Guillaume Melquiond | |
| 2016-06-20 | Reference Manual / Extraction: the original example command no longer works ↵ | Matej Kosik | |
| with recent Coq | |||
| 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-04-28 | Update tutorial (fix bug #4699). | Guillaume Melquiond | |
| 2016-04-12 | FIX: HTML version of Chapter 4 of the Reference Manual | Matej Kosik | |
| 2016-04-12 | TYPOGRAPHY: adding missing \noindent macros | Matej Kosik | |
| 2016-02-24 | Document Hint Mode, cleanup Hint doc. | Matthieu Sozeau | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-20 | Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500. | Maxime Dénès | |
| 2016-01-20 | Documenting Set Bullet Behavior. | Hugo Herbelin | |
| This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it. | |||
| 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-15 | Thanks Hugo, but let's remain factual. | Maxime Dénès | |
| 2016-01-13 | MMaps: remove it from final 8.5 release, since this new library isn't mature ↵ | Pierre Letouzey | |
| enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now. | |||
| 2016-01-12 | Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics. | Hugo Herbelin | |
| 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 | |
| 2016-01-06 | Fix description of command-line options in the manual. | Guillaume Melquiond | |
| 2015-12-16 | Updating credits. | Hugo Herbelin | |
| 2015-12-16 | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable". | Guillaume Melquiond | |
| 2015-12-15 | Proof using: do not clear unused section hyps automatically | Enrico Tassi | |
| The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account. | |||
| 2015-12-14 | Fix \label which was meants to be \ref in doc of CIC terms. | Maxime Dénès | |
| 2015-12-14 | Remove a mention of Set Virtual Machine in doc. | Maxime Dénès | |
| 2015-12-14 | Moved proof_admitted to its own file, named "AdmitAxiom.v". | Maxime Dénès | |
| 2015-12-12 | Extraction: documentation of the new option Unset Extraction SafeImplicits | Pierre Letouzey | |
| 2015-12-12 | Indexing and documenting some options. | Pierre-Marie Pédrot | |
| 2015-12-11 | Remove Set Virtual Machine from doc, since the command itself has been removed. | Maxime Dénès | |
| 2015-12-10 | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | |
| Marking it as experimental. | |||
| 2015-12-10 | Refman, ch. 4: A few fixes. | Hugo Herbelin | |
| 2015-12-10 | ENH: redundant examples were removed | Matej Kosik | |
| 2015-12-10 | FIX: wrong reference to a figure | Matej Kosik | |
| 2015-12-10 | CLEANUP: putting examples inside "figure" environment | Matej Kosik | |
| 2015-12-10 | ENH: The definition of the "_ ; _" operation on local context was added. | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY: adjustments | Matej Kosik | |
| 2015-12-10 | PROPOSITION: the side-condition was made more specific. | Matej Kosik | |
| 2015-12-10 | PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]' | Matej Kosik | |
| 2015-12-10 | PROPOSITION: Added an explicit definition of the notation for enriching the ↵ | Matej Kosik | |
| global environment (we use throughout the document) | |||
| 2015-12-10 | PROPOSITION: Added "if" and "then" words missing in the original sentence. | Matej Kosik | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |