aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Documenting Hint Resolve -> and <- variants.Gravatar Théo Zimmermann2016-10-19
| | | | These variants are from 8.3 but were never documented except in CHANGES.
* Making the doc of auto hints more precise.Gravatar Théo Zimmermann2016-10-19
| | | | | | | | | | 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.
* Extending the doc with a general summary of auto variants.Gravatar Théo Zimmermann2016-10-18
| | | | | This way of giving the summary avoids redundancy as much as possible. It is helpful for the auto-completion of Company-Coq of @cpitclaudel.
* Document info_auto.Gravatar Théo Zimmermann2016-10-18
| | | | | Now that this tactic has been fixed (commit 58d1381), it needed to get documented.
* Improve the documentation of eauto.Gravatar Théo Zimmermann2016-10-18
| | | | | | | | 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.
* Fixing #4887 (confusion between using and with in documentation of firstorder).Gravatar Hugo Herbelin2016-09-27
|
* Replace { command ; } with ( command )Gravatar Erik Martin-Dorel2016-09-19
| | | | | as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output.
* Fix typos in RefMan-uti.tex.Gravatar Erik Martin-Dorel2016-09-19
| | | | | | - 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.
* Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
|
* Reference Manual / Extraction: the original example command no longer works ↵Gravatar Matej Kosik2016-06-20
| | | | with recent Coq
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | 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.
* Update tutorial (fix bug #4699).Gravatar Guillaume Melquiond2016-04-28
|
* FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
|
* TYPOGRAPHY: adding missing \noindent macrosGravatar Matej Kosik2016-04-12
|
* Document Hint Mode, cleanup Hint doc.Gravatar Matthieu Sozeau2016-02-24
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Gravatar Maxime Dénès2016-01-20
|
* Documenting Set Bullet Behavior.Gravatar Hugo Herbelin2016-01-20
| | | | | | This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it.
* Clarifying the documentation of tactics "cbv" and "lazy".Gravatar Hugo Herbelin2016-01-20
| | | | Following a discussion on coq-club on Jan 13, 2016.
* Thanks Hugo, but let's remain factual.Gravatar Maxime Dénès2016-01-15
|
* MMaps: remove it from final 8.5 release, since this new library isn't mature ↵Gravatar Pierre Letouzey2016-01-13
| | | | | | | | 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.
* Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Gravatar Hugo Herbelin2016-01-12
|
* Documenting dtauto and dintuition.Gravatar Hugo Herbelin2016-01-12
|
* Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Gravatar Hugo Herbelin2016-01-12
|
* Documenting option 'Set Bracketing Last Introduction Pattern'.Gravatar Hugo Herbelin2016-01-12
|
* restore documentation of admitGravatar Enrico Tassi2016-01-12
|
* Fix description of command-line options in the manual.Gravatar Guillaume Melquiond2016-01-06
|
* Updating credits.Gravatar Hugo Herbelin2015-12-16
|
* Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
|
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
| | | | | | 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.
* Fix \label which was meants to be \ref in doc of CIC terms.Gravatar Maxime Dénès2015-12-14
|
* Remove a mention of Set Virtual Machine in doc.Gravatar Maxime Dénès2015-12-14
|
* Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14
|
* Extraction: documentation of the new option Unset Extraction SafeImplicitsGravatar Pierre Letouzey2015-12-12
|
* Indexing and documenting some options.Gravatar Pierre-Marie Pédrot2015-12-12
|
* Remove Set Virtual Machine from doc, since the command itself has been removed.Gravatar Maxime Dénès2015-12-11
|
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
| | | | Marking it as experimental.
* Refman, ch. 4: A few fixes.Gravatar Hugo Herbelin2015-12-10
|
* ENH: redundant examples were removedGravatar Matej Kosik2015-12-10
|
* FIX: wrong reference to a figureGravatar Matej Kosik2015-12-10
|
* CLEANUP: putting examples inside "figure" environmentGravatar Matej Kosik2015-12-10
|
* ENH: The definition of the "_ ; _" operation on local context was added.Gravatar Matej Kosik2015-12-10
|
* TYPOGRAPHY: adjustmentsGravatar Matej Kosik2015-12-10
|
* PROPOSITION: the side-condition was made more specific.Gravatar Matej Kosik2015-12-10
|
* PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'Gravatar Matej Kosik2015-12-10
|
* PROPOSITION: Added an explicit definition of the notation for enriching the ↵Gravatar Matej Kosik2015-12-10
| | | | global environment (we use throughout the document)
* PROPOSITION: Added "if" and "then" words missing in the original sentence.Gravatar Matej Kosik2015-12-10
|
* PROPOSITION: Example was simplifiedGravatar Matej Kosik2015-12-10
|
* DONEGravatar Matej Kosik2015-12-10
|
* COMMENT: questionGravatar Matej Kosik2015-12-10
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 04:42:35 +0000