coq - The formal proof system

Age	Commit message (Expand)	Author
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
2008-07-26	Even better test for choosing rewrite or setoid_rewrite.	msozeau
2008-07-25	A better test for relations being setoids or not: do leibniz rewrite iff	msozeau
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-06-22	Rename obligations_tactic to obligation_tactic and fix bugs #1893.	msozeau
2008-06-21	Correction petit bug sur révision 11159 (res_pf fait un effet de bord	herbelin
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-04-17	Bug squashing day !	msozeau
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-04-04	Quelques améliorations des intro patterns:	herbelin
2008-03-07	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau
2008-03-06	Plug the new setoid implemtation in, leaving the original one commented	msozeau
2008-03-01	Rework on rich forms of rewrite	letouzey
2007-10-05	Added the automatic generation of the boolean equality if possible and the	vsiles
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-09-06	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin
2007-07-06	Adding a syntax for "n-ary" rewrite:	letouzey
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest