coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix some typos.	Guillaume Melquiond	2015-12-07
*	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
*	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin	2015-12-02
*	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau	2015-11-04
*	Fixing error messages about Hint.	Hugo Herbelin	2015-10-02
*	Improving reference manual in that auto uses simple apply rather than apply.	Hugo Herbelin	2015-10-02
*	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin	2015-08-02
*	Fix some broken Coq scripts in the documentation.	Guillaume Melquiond	2015-07-30
*	Document Set/Print Firstorder Solver option.	Matthieu Sozeau	2015-07-07
*	Documenting Set Regular Subst Tactic (though unsure this is worth the	Hugo Herbelin	2015-05-13
*	Documenting the Loose Hint Behavior flag.	Pierre-Marie Pédrot	2015-05-13
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
*	Preprend Fail to all the expected failures in the documentation.	Guillaume Melquiond	2015-03-05
*	Separate index for vernacular options.	Maxime Dénès	2015-02-17
*	Remove non-existing Tactic Definition command from index.	Maxime Dénès	2015-02-17
*	Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.	Hugo Herbelin	2015-02-16
*	Fix documentation of generalize. (Fix for bug #4015)	Guillaume Melquiond	2015-02-10
*	Fix some documentation typo.	Guillaume Melquiond	2015-02-10
*	Fix some broken Coq scripts in the reference manual.	Guillaume Melquiond	2015-01-29
*	Reference Manual: Documenting new printing of evars and new effect of	Hugo Herbelin	2015-01-24
*	Document native_compute.	Maxime Dénès	2015-01-08
*	refman: avoid label names with whitespace (unsupported in html)	Pierre Letouzey	2014-12-09
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Fixing doc of Functional Induction.	Hugo Herbelin	2014-11-07
*	Documenting the change of semantics of the replace tactic.	Pierre-Marie Pédrot	2014-11-04
*	Addressing report #3279 (inconsistency of behavior of the -> and <-	Hugo Herbelin	2014-10-24
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
*	Removing "eqn:" for "induction" in reference manual.	Hugo Herbelin	2014-09-10
*	Doc: [revgoals].	Arnaud Spiwack	2014-09-08
*	Little fix in documentation of inversion.	Hugo Herbelin	2014-09-07
*	Cbn in refman	Pierre Boutillier	2014-09-03
*	"allows to", like "allowing to", is improper	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
*	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
*	Typos.	Hugo Herbelin	2014-07-31
*	Document swap tactic.	Arnaud Spiwack	2014-07-25
*	Document cycle tactic.	Arnaud Spiwack	2014-07-25
*	Warns about inconsistency of generated name in evars and goals.	Arnaud Spiwack	2014-07-25
*	More on injection over a projectable "existT". - Fixing syntax "injection ......	Hugo Herbelin	2014-05-31
*	Fix for bug #3107.	Guillaume Melquiond	2014-04-04
*	fixing Function doc	Julien Forest	2014-04-04
*	Fix Bug 3131 + Really drop mentions of info in refman.	Pierre Boutillier	2014-04-02
*	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot	2013-12-11
*	Silence some warning about references in documentation.	Guillaume Melquiond	2013-12-03
*	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	aspiwack	2013-11-02
*	Adds a tactic give_up.	aspiwack	2013-11-02
*	A tactic shelve_unifiable.	aspiwack	2013-11-02
*	Adds a shelve tactic.	aspiwack	2013-11-02