coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack	2012-02-07
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	A new tactic is_var to check whether a term is a goal/section variable	letouzey	2011-10-07
*	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin	2011-09-26
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Rename the "raw" argument extension into "glob"	glondu	2010-12-27
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Add tactic has_evar (#2433)	glondu	2010-12-02
*	Add tactic is_evar (Closes: #2433)	glondu	2010-12-02
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Adding the destauto tactic, that reduces match by destructing matched	courtieu	2010-07-22
*	Finish adding out-of-the-box support for camlp4	letouzey	2010-07-09
*	Made "replace" accepts open terms on its left-hand-side.	herbelin	2010-06-28
*	Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).	herbelin	2010-06-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau	2010-01-30
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Updated compatibility for rewriting equality proofs that are dependent	herbelin	2009-12-12
*	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau	2009-11-24
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	- 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-08-06
*	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey	2009-07-24
*	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau	2009-06-30
*	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin	2009-05-20
*	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin	2009-05-09
*	Rewrite autorewrite to use a dnet indexed by the left-hand sides (or	msozeau	2009-04-14
*	Getting rid of the previous implementation of setoid_rewrite which was	msozeau	2009-01-18
*	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau	2008-12-16
*	About "apply in":	herbelin	2008-12-09
*	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau	2008-11-05
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	Various little improvements:	msozeau	2008-09-25