coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-01	Switched to "standardized" names for the properties of eq and	herbelin
2009-01-01	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin
2008-12-26	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin
2008-12-18	- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a side	herbelin
2008-12-09	About "apply in":	herbelin
2008-11-23	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
2008-11-05	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
2008-09-12	Add a type argument to letin_tac instead of using casts and recomputing	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-28	Fix wrong environment bug in test for setoid_rewrite or rewrite.	msozeau