coq - The formal proof system

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