coq - The formal proof system

Age	Commit message (Expand)	Author
2012-02-07	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack
2011-11-17	Merge subinstances branch by me and Tom Prince.	msozeau
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-10-07	A new tactic is_var to check whether a term is a goal/section variable	letouzey
2011-09-26	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin
2011-06-18	Relaxed the constraint introduced in r14190 that froze the existing	herbelin
2011-02-14	- Fix treatment of globality flag for typeclass instance hints (they	msozeau
2010-12-27	Rename the "raw" argument extension into "glob"	glondu
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-12-02	Add tactic has_evar (#2433)	glondu
2010-12-02	Add tactic is_evar (Closes: #2433)	glondu
2010-11-07	Delayed the evar normalization in error messages to the last minute	herbelin
2010-09-30	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu
2010-09-28	Remove some occurrences of "open Termops"	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Adding the destauto tactic, that reduces match by destructing matched	courtieu
2010-07-09	Finish adding out-of-the-box support for camlp4	letouzey
2010-06-28	Made "replace" accepts open terms on its left-hand-side.	herbelin
2010-06-22	Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-01-30	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-11-24	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-06	Move out JMeq of subst for compatibility (it affects e.g. the	herbelin
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-06-30	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-14	Rewrite autorewrite to use a dnet indexed by the left-hand sides (or	msozeau
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2008-12-16	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau
2008-12-09	About "apply in":	herbelin
2008-11-05	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-09-25	Various little improvements:	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-28	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau
2008-07-22	New tactics [conv] to test convertibility (actually, unification) of two	msozeau
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2008-04-27	Correction du bug des types singletons pas sous-type de Set	herbelin