coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Documenting the [Variant] type definition and the [Nonrecursive Elimination S...	Arnaud Spiwack	2014-09-04
*	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier	2014-09-03
*	Improve RefMan section about Coq_makefile	Pierre Boutillier	2014-09-03
*	Update RefMan with respect to new loadpath management	Pierre Boutillier	2014-09-03
*	Cbn in refman	Pierre Boutillier	2014-09-03
*	coqworkmgr	Enrico Tassi	2014-09-02
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Grammar: "allowing to" is not proper English	Jason Gross	2014-08-25
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Slight simplification of naming of tactics in equality.ml (hopefully).	Hugo Herbelin	2014-08-18
*	Removing documentation related to the deprecated State machinery.	Pierre-Marie Pédrot	2014-08-16
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	2014-08-05
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Adding a syntax "enough" for the variant of "assert" with the order of	Hugo Herbelin	2014-08-05
*	Making references to Proof General and CoqIDE uniform in Reference Manual.	Hugo Herbelin	2014-08-05
*	Chapter 4 of reference manual: Fixing asymmetric patterns error +	Hugo Herbelin	2014-08-05
*	Documentation: a simple example for [numgoals].	Arnaud Spiwack	2014-08-05
*	Documentation of [uconstr]: typesetting.	Arnaud Spiwack	2014-08-05
*	Documentation: refine accept uconstr arguments.	Arnaud Spiwack	2014-08-05
*	Doc: uconstr now has a tactic notation entry.	Arnaud Spiwack	2014-08-05
*	Chapter 4: Fixing ambiguity about whether the return predicate refers	Hugo Herbelin	2014-08-03
*	Document [> … ].	Arnaud Spiwack	2014-08-01
*	Fix English spelling -> American spelling in doc.	Arnaud Spiwack	2014-08-01
*	Document [numgoals] and [guard].	Arnaud Spiwack	2014-08-01
*	Typos.	Hugo Herbelin	2014-07-31
*	Document untyped terms in tactics.	Arnaud Spiwack	2014-07-29
*	Document swap tactic.	Arnaud Spiwack	2014-07-25
*	Document cycle tactic.	Arnaud Spiwack	2014-07-25
*	Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...	Arnaud Spiwack	2014-07-25
*	Warns about inconsistency of generated name in evars and goals.	Arnaud Spiwack	2014-07-25
*	More documentation of universes.	Matthieu Sozeau	2014-07-25
*	Start documenting universe polymorphism.	Matthieu Sozeau	2014-07-24
*	Derive plugin: document new syntax.	Arnaud Spiwack	2014-07-23
*	Documenting the changes of Locate semantics.	Pierre-Marie Pédrot	2014-07-21
*	Added a (constructive) proof of Weak Konig's lemma for decidable trees.	Hugo Herbelin	2014-07-15
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"	Hugo Herbelin	2014-07-01
*	Avoid scanning .coq-native directories when building the library index.	Guillaume Melquiond	2014-06-26
*	Fix documentation.	Guillaume Melquiond	2014-06-26
*	Fixing grammar in doc of Opaque as proposed by Jason (#3389).	Hugo Herbelin	2014-06-21
*	Deprecate useless option -quality.	Guillaume Melquiond	2014-06-13
*	Remove documentation for the unsupported options -byte and -opt.	Guillaume Melquiond	2014-06-13
*	Deprecate options -dont, -lazy, -force-load-proofs.	Guillaume Melquiond	2014-06-13
*	More on injection over a projectable "existT". - Fixing syntax "injection ......	Hugo Herbelin	2014-05-31
*	Typo reference manual	Hugo Herbelin	2014-05-08
*	- Fix index-list to show computational relations for rewriting files.	Matthieu Sozeau	2014-05-06
*	Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)	Guillaume Melquiond	2014-04-28
*	Completing text of the question on conservativity of CIC over CC (bug #2697).	Hugo Herbelin	2014-04-05
*	Fix for bug #3107.	Guillaume Melquiond	2014-04-04