aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2014-11-12Document (some) Proof using syntax + the new Optimize commandsEnrico Tassi
2014-11-07Fixing doc of Functional Induction.Hugo Herbelin
2014-11-04Documenting the change of semantics of the replace tactic.Pierre-Marie Pédrot
2014-11-01Document [Info] command.Arnaud Spiwack
2014-10-24Addressing report #3279 (inconsistency of behavior of the -> and <-Hugo Herbelin
2014-10-24Fix typo in documentation of the [repeat] tactical.Arnaud Spiwack
2014-10-22Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Enrico Tassi
2014-10-16More fallout from elisp renameAnders Kaseorg
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 21:37:19 +0000