aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* TYPOGRAPHY: correction of one particular error in the Reference ManualGravatar Matej Kosik2015-12-18
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\
| * 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
* | Simplifying documentation of "assert form as pat".Gravatar Hugo Herbelin2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * 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
| * 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 g...Gravatar Matej Kosik2015-12-10
| * 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
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * TYPOGRAPHYGravatar Matej Kosik2015-12-10
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * COMMENT: to doGravatar Matej Kosik2015-12-10
| * GRAMMAR: added punctuationGravatar Matej Kosik2015-12-10
| * CLEANUP PROPOSITION: rephrasing the original idea in a simpler wayGravatar Matej Kosik2015-12-10
| * CLEANUP PROPOSITION: existing example was removed because it is not urgently ...Gravatar Matej Kosik2015-12-10
| * ENH: existing example was changed so that it is now linked to the results sho...Gravatar Matej Kosik2015-12-10
| * ENH: an existing example was further expanded.Gravatar Matej Kosik2015-12-10
| * CLEANUP: Existing example was removed.Gravatar Matej Kosik2015-12-10
| * ENH: existing example was expandedGravatar Matej Kosik2015-12-10
| * ENH: define the meaning of 'p'Gravatar Matej Kosik2015-12-10
| * CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive definit...Gravatar Matej Kosik2015-12-10
| * CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive de...Gravatar Matej Kosik2015-12-10
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * CLEANUP: removing a superfluous indexGravatar Matej Kosik2015-12-10
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * COMMENT: questionGravatar Matej Kosik2015-12-10
| * GRAMMARGravatar Matej Kosik2015-12-10