aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* 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
* Fix documentation.Gravatar Guillaume Melquiond2014-06-26
* Fixing grammar in doc of Opaque as proposed by Jason (#3389).Gravatar Hugo Herbelin2014-06-21
* Deprecate useless option -quality.Gravatar Guillaume Melquiond2014-06-13
* Remove documentation for the unsupported options -byte and -opt.Gravatar Guillaume Melquiond2014-06-13
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Typo reference manualGravatar Hugo Herbelin2014-05-08
* - Fix index-list to show computational relations for rewriting files.Gravatar Matthieu Sozeau2014-05-06
* Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Gravatar Guillaume Melquiond2014-04-28
* Completing text of the question on conservativity of CIC over CC (bug #2697).Gravatar Hugo Herbelin2014-04-05
* Fix for bug #3107.Gravatar Guillaume Melquiond2014-04-04