coq - The formal proof system

Age	Commit message (Expand)	Author
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-03-05	Fixing injection bug #2493 (regression introduced by fixing injection	herbelin
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-11-07	Delayed the evar normalization in error messages to the last minute	herbelin
2010-10-27	correction of bug #2414 (report of r 13586)	jforest
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
2010-09-17	In the computation of missing arguments for apply, accept that the	herbelin
2010-09-13	Fix unescaped end-of-lines (OCaml warning 29)	glondu
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-05-29	New pass on inductive schemes	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-05	Improving compatibility between 8.2 and 8.3	herbelin
2010-03-27	Applied greenrd's patch to fix bug 2255 (injection failed to	herbelin
2009-12-28	Safer, though ad hoc, approach to re-interpretation of the argument of	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-14	Improved strategy for rewriting lemma possibly depending because of evars.	herbelin
2009-12-13	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin
2009-12-13	Completion of r12580 (better rendering of dependent rewrite and inversion).	herbelin
2009-12-13	Revision 12557 continued (better rendering of dependent rewrite)	herbelin
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-12-12	Improved the rendering of "dependent rewrite" and hence of "inversion"	herbelin
2009-12-03	Restored rewriting of JMeq using JMeq_rect and co when the domains are the same	herbelin
2009-11-12	Addendum to revision 12501.	herbelin
2009-11-11	Backtracking on the use of automatically generated schemes for	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-09	Quick fix for restoring a left-to-right rewriting lemma compatible	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-28	Remove old compatibility stuff (Tacred.nf)	glondu
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-09-27	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin
2009-09-27	Delay the choice of eliminator in destruct/induction until we know if	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-09	Stop trying to search if the relation is declared as a [RewriteRelation]	msozeau
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-08-06	Move out JMeq of subst for compatibility (it affects e.g. the	herbelin
2009-08-04	Fixed subst failing when a truly heterogeneous JMeq hyp is in the	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-30	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau
2009-06-16	Reimplementation of leibniz rewrite to control the instantiation of the	msozeau
2009-04-08	Some dead code removal + cleanups	letouzey
2009-03-20	Fixes to make Ynot compile with the trunk:	msozeau
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-06	pushed evar reduction in kernel	barras