coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\
\| *	Fix incompleteness of conversion used by evarconv	Matthieu Sozeau	2015-06-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	Fixing incompatibility introduced with simpl in commit 364decf59c1 (or	Hugo Herbelin	2015-06-23
* \|	Turning "Set Regular Subst Tactic" on by default (for 8.6).	Hugo Herbelin	2015-05-15
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Extraction: fix the detection of the "polyprop" situation	Pierre Letouzey	2015-05-12
\| *	Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).	Hugo Herbelin	2015-05-09
\| *	Fixing treatment of recursive equations damaged by 857e82b2ca0d1.	Hugo Herbelin	2015-05-06
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Fixing test-suite.	Pierre-Marie Pédrot	2015-04-01
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin	2015-03-25
\| *	Another example about the consequence of a wrong computation of the	Hugo Herbelin	2015-03-25
\| *	Fixing computation of non-recursively uniform arguments in the	Hugo Herbelin	2015-03-24
\| *	Fixing wrong rel_context in checking positivity condition.	Hugo Herbelin	2015-03-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	Qed export -> Qed exporting	Enrico Tassi	2015-03-22
* \|	Merge branch 'v8.5' into trunk	Arnaud Spiwack	2015-03-13
\|\\|
\| *	Add some tests for tryif	Jason Gross	2015-03-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	Add a test-suite file ensuring coinductives with primitive projections	Matthieu Sozeau	2015-03-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-28
\|\\|
\| *	Fixing first part of bug #3210 (inference of pattern-matching return	Hugo Herbelin	2015-02-27
* \|	Other tests for decl mode, coming from reference manual.	Hugo Herbelin	2015-02-24
\|/
*	Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.	Hugo Herbelin	2015-02-23
*	Fixing occur-check which was too strong in unification.ml.	Hugo Herbelin	2015-02-23
*	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
*	Adding a test-suite for tactic notation naming.	Pierre-Marie Pédrot	2015-02-11
*	Revert "Fix files in test-suite having to do with Require inside modules."	Maxime Dénès	2015-01-17
*	Univs: Fix alias computation for VMs, computation of normal form of	Matthieu Sozeau	2015-01-17
*	Fix files in test-suite having to do with Require inside modules.	Maxime Dénès	2015-01-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Extraction: discard code unnecessary to fulfill a module signature	Pierre Letouzey	2015-01-11
*	An optimization in the use of unification candidates so as to get the	Hugo Herbelin	2015-01-01
*	Better doc and a few fixes for Proof using.	Enrico Tassi	2014-12-19
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
*	fix bug #2447 in congruence	Pierre Corbineau	2014-12-16
*	Fixing orientation of postponed subtyping problems.	Hugo Herbelin	2014-12-10
*	Improving evar restriction (this is a risky change, as I remember a	Hugo Herbelin	2014-12-07
*	Take benefit of improved name preservation of evars in e2fa65fcc.	Hugo Herbelin	2014-12-04
*	When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if	Hugo Herbelin	2014-12-02
*	Adapting to current semantics of "simpl non-evaluable-cst"	Hugo Herbelin	2014-11-25
*	Experimenting using unification when matching evar/meta free subterms	Hugo Herbelin	2014-11-25
*	Add test-suite file for dependent rewriting example by Vadim Zaliva and	Matthieu Sozeau	2014-11-22
*	Fixing a little bug with nested but convertible occurrences in "destruct at".	Hugo Herbelin	2014-11-18
*	Fixing detection of occurrences in the presence of nested subterms for	Hugo Herbelin	2014-11-18
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16