Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 | |
|\| | | ||||
| * | | 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 | 2016-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". | Hugo Herbelin | 2016-01-20 | |
| | | | | | | | | | | | | Following a discussion on coq-club on Jan 13, 2016. | |||
| * | | Thanks Hugo, but let's remain factual. | Maxime Dénès | 2016-01-15 | |
| | | | ||||
* | | | Updating and improving the documentation of intros patterns. | Hugo Herbelin | 2016-01-14 | |
| | | | | | | | | | | | | In particular, documenting bracketing of last pattern on by default. | |||
| * | | MMaps: remove it from final 8.5 release, since this new library isn't mature ↵ | Pierre Letouzey | 2016-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. | |||
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-13 | |
|\| | | ||||
| * | | 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-12 | |
| | | | ||||
| * | | Fix description of command-line options in the manual. | Guillaume Melquiond | 2016-01-06 | |
| | | | ||||
* | | | TYPOGRAPHY: correction of one particular error in the Reference Manual | Matej Kosik | 2015-12-18 | |
| | | | ||||
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-17 | |
|\| | | ||||
| * | | Updating credits. | Hugo Herbelin | 2015-12-16 | |
| | | | ||||
| * | | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable". | Guillaume Melquiond | 2015-12-16 | |
| | | | ||||
| * | | Proof using: do not clear unused section hyps automatically | Enrico Tassi | 2015-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. | |||
* | | | Simplifying documentation of "assert form as pat". | Hugo Herbelin | 2015-12-15 | |
| | | | ||||
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2015-12-15 | |
|\| | | ||||
| * | | 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-14 | |
| | | | ||||
| * | | 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-12 | |
| | | | ||||
* | | | Merge branch 'v8.5' | 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-11 | |
| | | | ||||
| * | | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | 2015-12-10 | |
| | | | | | | | | | | | | Marking it as experimental. | |||
| * | | 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 | 2015-12-10 | |
| | | | | | | | | | | | | global environment (we use throughout the document) | |||
| * | | PROPOSITION: Added "if" and "then" words missing in the original sentence. | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | PROPOSITION: Example was simplified | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | DONE | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | COMMENT: question | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | COMMENT: question | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | COMMENT: question | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | COMMENT: question | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | TYPOGRAPHY | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | COMMENT: question | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | COMMENT: question | Matej Kosik | 2015-12-10 | |
| | | | ||||
| * | | COMMENT: to do | Matej Kosik | 2015-12-10 | |
| | | |