coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	CHANGES: mention "Optimize (Heap\|Proof)"	Enrico Tassi	2015-01-10
*	Update + English in CHANGES	Hugo Herbelin	2015-01-08
*	Start credits for 8.5.	Matthieu Sozeau	2015-01-08
*	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu	2015-01-08
*	Document native_compute.	Maxime Dénès	2015-01-08
*	rename: vi -> vio	Enrico Tassi	2015-01-06
*	Document the new behavior of lazymatch.	Guillaume Melquiond	2014-12-30
*	more CHANGES	Enrico Tassi	2014-12-30
*	Minor modification of CHANGE.	Pierre Courtieu	2014-12-23
*	Better doc and a few fixes for Proof using.	Enrico Tassi	2014-12-19
*	In CHANGES, alerting about stronger check on notation level modifiers.	Hugo Herbelin	2014-12-16
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Documenting the Set Refine Instance Mode.	Pierre-Marie Pédrot	2014-11-30
*	Hopefully the last word on having "simpl f" complying with the	Hugo Herbelin	2014-11-18
*	Fixing detection of occurrences in the presence of nested subterms for	Hugo Herbelin	2014-11-18
*	Documenting use of colors in Coq.	Pierre-Marie Pédrot	2014-11-17
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Updating CHANGES (evars as ident).	Hugo Herbelin	2014-11-11
*	American spelling + layout in CHANGES.	Hugo Herbelin	2014-11-11
*	Fixing careless name confusion in CHANGES.	Pierre-Marie Pédrot	2014-11-04
*	Documenting the change of semantics of the replace tactic.	Pierre-Marie Pédrot	2014-11-04
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Documenting some incompatibilities in (non) Import of ML tactics,	Hugo Herbelin	2014-10-24
*	Addressing report #3279 (inconsistency of behavior of the -> and <-	Hugo Herbelin	2014-10-24
*	CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin...	Arnaud Spiwack	2014-10-22
*	Mentioning incompatibility shown in #3718 and coming from #3050	Hugo Herbelin	2014-10-13
*	Documenting option -type-in-type.	Hugo Herbelin	2014-09-29
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
*	Documenting the new Undo semantics	Enrico Tassi	2014-09-09
*	Removing the documentation of the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	CHANGES: existential variables are always "substituted" in the new tactic eng...	Arnaud Spiwack	2014-09-08
*	CHANGES: Ltac's [refine] accepts [uconstr].	Arnaud Spiwack	2014-09-08
*	CHANGES: [revgoals].	Arnaud Spiwack	2014-09-08
*	CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].	Arnaud Spiwack	2014-09-08
*	CHANGES: binder names from Ltac identifiers.	Arnaud Spiwack	2014-09-08
*	"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
*	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
*	A new step in the new "standard" naming policy for propositional hypotheses	Hugo Herbelin	2014-08-05
*	CHANGES: [>…].	Arnaud Spiwack	2014-08-01
*	CHANGES: [numgoals] and [guard].	Arnaud Spiwack	2014-08-01
*	Making the error message about bullets more precise.	Pierre Courtieu	2014-07-31
*	CHANGES: untyped terms in tactics	Arnaud Spiwack	2014-07-29
*	CHANGES: cycle and swap.	Arnaud Spiwack	2014-07-25
*	CHANGES: yellow in Coqide.	Arnaud Spiwack	2014-07-25