coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	An optimization of tactic constructor.	Hugo Herbelin	2017-09-19
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	Fixing complexity file f_equal.v.	Hugo Herbelin	2015-11-06
*	Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan	Hugo Herbelin	2015-11-06
*	Fixing complexity tests for #4076.	Maxime Dénès	2015-02-26
*	Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).	Hugo Herbelin	2015-02-25
*	Compensating 6fd763431 on postponing subtyping evar-evar problems.	Hugo Herbelin	2015-02-23
*	Last test-suite not in Symmetric Patterns syntax	pboutill	2013-01-21
*	Minor fixes in the test-suite after my recent commits	letouzey	2012-07-06
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	Fixing format of complexity bug Notations.v.	herbelin	2011-12-17
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
*	Optimizing the compilation of unused aliases in pattern-matching.	herbelin	2011-11-21
*	Fixes in the test-suite after modularisation of ZArith and co	letouzey	2011-05-06
*	fixed guard check with commutative cuts	barras	2010-05-20
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
*	Small things about coqdoc + fixing lettuple.v test (part of bug #2289)	herbelin	2010-03-30
*	Fixing bug #2279 (printing nested let-in was in exponential time)	herbelin	2010-03-27
*	fixed minor pbs with test cases	barras	2010-03-12
*	introduced lazy computation of size info in the guard condition	barras	2010-03-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	illegal tactic application was having Ltac interpreter loop	barras	2009-03-04
*	commited complexity test for exponential behavior of unification	barras	2009-02-09
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq	letouzey	2008-07-09
*	Strategy commands are now exported	barras	2008-05-22
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	Ajout d'un test de complexité de injection (cf bug 1173)	herbelin	2007-04-14
*	Pas de solution à court terme pour ce problème de complexité	herbelin	2007-01-28
*	Correction petits bugs du check de la test-suite	herbelin	2006-12-28
*	Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...	herbelin	2006-12-12
*	Test bug #932	herbelin	2006-12-12
*	Ajout test setoid_rewrite (cf bug #1176); anglicisation	herbelin	2006-11-01
*	Ajout d'un répertoire de test de la complexité	herbelin	2006-10-06