aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2014-10-03Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Hugo Herbelin
2014-10-03Removing deactivated command Show Tree.Hugo Herbelin
2014-09-29typoEnrico Tassi
2014-09-29Documenting option -type-in-type.Hugo Herbelin
2014-09-18seems to fix a looping coq-tex (when compiled with camlp4)Pierre Boutillier
2014-09-11Fixing bug #3605.Pierre-Marie Pédrot
2014-09-11Removing remaining documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
2014-09-10Removing "eqn:" for "induction" in reference manual.Hugo Herbelin
2014-09-09Documenting the new Undo semanticsEnrico Tassi
2014-09-08Removing the documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-08Doc: [revgoals].Arnaud Spiwack
2014-09-07Little fix in documentation of inversion.Hugo Herbelin
2014-09-04Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Arnaud Spiwack
2014-09-03sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texPierre Boutillier
2014-09-03Improve RefMan section about Coq_makefilePierre Boutillier
2014-09-03Update RefMan with respect to new loadpath managementPierre Boutillier
2014-09-03Cbn in refmanPierre Boutillier
2014-09-02coqworkmgrEnrico Tassi
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-08-05Uncountably many bullets (+,-,*,++,--,**,+++,...).Hugo Herbelin
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-08-05Making references to Proof General and CoqIDE uniform in Reference Manual.Hugo Herbelin
2014-08-05Chapter 4 of reference manual: Fixing asymmetric patterns error +Hugo Herbelin
2014-08-05Documentation: a simple example for [numgoals].Arnaud Spiwack
2014-08-05Documentation of [uconstr]: typesetting.Arnaud Spiwack
2014-08-05Documentation: refine accept uconstr arguments.Arnaud Spiwack
2014-08-05Doc: uconstr now has a tactic notation entry.Arnaud Spiwack
2014-08-03Chapter 4: Fixing ambiguity about whether the return predicate refersHugo Herbelin
2014-08-01Document [> … ].Arnaud Spiwack
2014-08-01Fix English spelling -> American spelling in doc.Arnaud Spiwack
2014-08-01Document [numgoals] and [guard].Arnaud Spiwack
2014-07-31Typos.Hugo Herbelin
2014-07-29Document untyped terms in tactics.Arnaud Spiwack
2014-07-25Document swap tactic.Arnaud Spiwack
2014-07-25Document cycle tactic.Arnaud Spiwack
2014-07-25Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...Arnaud Spiwack
2014-07-25Warns about inconsistency of generated name in evars and goals.Arnaud Spiwack
2014-07-25More documentation of universes.Matthieu Sozeau
2014-07-24Start documenting universe polymorphism.Matthieu Sozeau
2014-07-23Derive plugin: document new syntax.Arnaud Spiwack
2014-07-21Documenting the changes of Locate semantics.Pierre-Marie Pédrot
2014-07-15Added a (constructive) proof of Weak Konig's lemma for decidable trees.Hugo Herbelin
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 20:33:24 +0000