coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of identifier	ppedrot	2012-12-14
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Monomorphization (tactics)	ppedrot	2012-11-25
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Continue killing hidden tactics : no more generated h_xxx	letouzey	2012-10-15
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	tactic is_fix, akin to is_evar, is_hyp, is_ ... family	pboutill	2012-05-31
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	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