Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | Documenting Set Bullet Behavior. | 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". | 2016-01-20 | ||
| | | | | | | | | | | | | Following a discussion on coq-club on Jan 13, 2016. | |||
| * | | Thanks Hugo, but let's remain factual. | 2016-01-15 | ||
| | | | ||||
* | | | Updating and improving the documentation of intros patterns. | 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 ↵ | 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' | 2016-01-13 | ||
|\| | | ||||
| * | | Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics. | 2016-01-12 | ||
| | | | ||||
| * | | Documenting dtauto and dintuition. | 2016-01-12 | ||
| | | | ||||
| * | | Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding". | 2016-01-12 | ||
| | | | ||||
| * | | Documenting option 'Set Bracketing Last Introduction Pattern'. | 2016-01-12 | ||
| | | | ||||
| * | | restore documentation of admit | 2016-01-12 | ||
| | | | ||||
| * | | Fix description of command-line options in the manual. | 2016-01-06 | ||
| | | | ||||
* | | | TYPOGRAPHY: correction of one particular error in the Reference Manual | 2015-12-18 | ||
| | | | ||||
* | | | Merge branch 'v8.5' | 2015-12-17 | ||
|\| | | ||||
| * | | Updating credits. | 2015-12-16 | ||
| | | | ||||
| * | | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable". | 2015-12-16 | ||
| | | | ||||
| * | | Proof using: do not clear unused section hyps automatically | 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". | 2015-12-15 | ||
| | | | ||||
* | | | Merge branch 'v8.5' | 2015-12-15 | ||
|\| | | ||||
| * | | Fix \label which was meants to be \ref in doc of CIC terms. | 2015-12-14 | ||
| | | | ||||
| * | | Remove a mention of Set Virtual Machine in doc. | 2015-12-14 | ||
| | | | ||||
| * | | Moved proof_admitted to its own file, named "AdmitAxiom.v". | 2015-12-14 | ||
| | | | ||||
| * | | Extraction: documentation of the new option Unset Extraction SafeImplicits | 2015-12-12 | ||
| | | | ||||
| * | | Indexing and documenting some options. | 2015-12-12 | ||
| | | | ||||
* | | | Merge branch 'v8.5' | 2015-12-11 | ||
|\| | | ||||
| * | | Remove Set Virtual Machine from doc, since the command itself has been removed. | 2015-12-11 | ||
| | | | ||||
| * | | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | 2015-12-10 | ||
| | | | | | | | | | | | | Marking it as experimental. | |||
| * | | Refman, ch. 4: A few fixes. | 2015-12-10 | ||
| | | | ||||
| * | | ENH: redundant examples were removed | 2015-12-10 | ||
| | | | ||||
| * | | FIX: wrong reference to a figure | 2015-12-10 | ||
| | | | ||||
| * | | CLEANUP: putting examples inside "figure" environment | 2015-12-10 | ||
| | | | ||||
| * | | ENH: The definition of the "_ ; _" operation on local context was added. | 2015-12-10 | ||
| | | | ||||
| * | | TYPOGRAPHY: adjustments | 2015-12-10 | ||
| | | | ||||
| * | | PROPOSITION: the side-condition was made more specific. | 2015-12-10 | ||
| | | | ||||
| * | | PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]' | 2015-12-10 | ||
| | | | ||||
| * | | PROPOSITION: Added an explicit definition of the notation for enriching the ↵ | 2015-12-10 | ||
| | | | | | | | | | | | | global environment (we use throughout the document) | |||
| * | | PROPOSITION: Added "if" and "then" words missing in the original sentence. | 2015-12-10 | ||
| | | | ||||
| * | | PROPOSITION: Example was simplified | 2015-12-10 | ||
| | | | ||||
| * | | DONE | 2015-12-10 | ||
| | | | ||||
| * | | COMMENT: question | 2015-12-10 | ||
| | | | ||||
| * | | COMMENT: question | 2015-12-10 | ||
| | | | ||||
| * | | COMMENT: question | 2015-12-10 | ||
| | | | ||||
| * | | COMMENT: question | 2015-12-10 | ||
| | | | ||||
| * | | TYPOGRAPHY | 2015-12-10 | ||
| | | | ||||
| * | | COMMENT: question | 2015-12-10 | ||
| | | | ||||
| * | | COMMENT: question | 2015-12-10 | ||
| | | | ||||
| * | | COMMENT: to do | 2015-12-10 | ||
| | | | ||||
| * | | GRAMMAR: added punctuation | 2015-12-10 | ||
| | | | ||||
| * | | CLEANUP PROPOSITION: rephrasing the original idea in a simpler way | 2015-12-10 | ||
| | | | ||||
| * | | CLEANUP PROPOSITION: existing example was removed because it is not urgently ↵ | 2015-12-10 | ||
| | | | | | | | | | | | | needed |