aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* typoGravatar Enrico Tassi2014-09-29
* Documenting option -type-in-type.Gravatar Hugo Herbelin2014-09-29
* seems to fix a looping coq-tex (when compiled with camlp4)Gravatar Pierre Boutillier2014-09-18
* Fixing bug #3605.Gravatar Pierre-Marie Pédrot2014-09-11
* Removing remaining documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-11
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Removing "eqn:" for "induction" in reference manual.Gravatar Hugo Herbelin2014-09-10
* Documenting the new Undo semanticsGravatar Enrico Tassi2014-09-09
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Doc: [revgoals].Gravatar Arnaud Spiwack2014-09-08
* Little fix in documentation of inversion.Gravatar Hugo Herbelin2014-09-07
* Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Gravatar Arnaud Spiwack2014-09-04
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
* Improve RefMan section about Coq_makefileGravatar Pierre Boutillier2014-09-03
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
* Cbn in refmanGravatar Pierre Boutillier2014-09-03
* coqworkmgrGravatar Enrico Tassi2014-09-02
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
* Chapter 4 of reference manual: Fixing asymmetric patterns error +Gravatar Hugo Herbelin2014-08-05
* Documentation: a simple example for [numgoals].Gravatar Arnaud Spiwack2014-08-05
* Documentation of [uconstr]: typesetting.Gravatar Arnaud Spiwack2014-08-05
* Documentation: refine accept uconstr arguments.Gravatar Arnaud Spiwack2014-08-05
* Doc: uconstr now has a tactic notation entry.Gravatar Arnaud Spiwack2014-08-05
* Chapter 4: Fixing ambiguity about whether the return predicate refersGravatar Hugo Herbelin2014-08-03
* Document [> … ].Gravatar Arnaud Spiwack2014-08-01
* Fix English spelling -> American spelling in doc.Gravatar Arnaud Spiwack2014-08-01
* Document [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Typos.Gravatar Hugo Herbelin2014-07-31
* Document untyped terms in tactics.Gravatar Arnaud Spiwack2014-07-29
* Document swap tactic.Gravatar Arnaud Spiwack2014-07-25
* Document cycle tactic.Gravatar Arnaud Spiwack2014-07-25
* Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...Gravatar Arnaud Spiwack2014-07-25
* Warns about inconsistency of generated name in evars and goals.Gravatar Arnaud Spiwack2014-07-25
* More documentation of universes.Gravatar Matthieu Sozeau2014-07-25
* Start documenting universe polymorphism.Gravatar Matthieu Sozeau2014-07-24
* Derive plugin: document new syntax.Gravatar Arnaud Spiwack2014-07-23
* Documenting the changes of Locate semantics.Gravatar Pierre-Marie Pédrot2014-07-21
* Added a (constructive) proof of Weak Konig's lemma for decidable trees.Gravatar Hugo Herbelin2014-07-15
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"Gravatar Hugo Herbelin2014-07-01
* Avoid scanning .coq-native directories when building the library index.Gravatar Guillaume Melquiond2014-06-26