coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin	2011-10-25
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin	2011-09-26
*	generic = on named_context replaced by named_context_equal	puech	2011-07-29
*	More work on error handling	letouzey	2011-05-17
*	Revert r14078 "Partial backtrack on the support for open terms in destruct/in...	gmelquio	2011-04-28
*	Partial backtrack on the support for open terms in destruct/induction:	gmelquio	2011-04-28
*	More informative anomaly.	herbelin	2011-04-14
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey	2011-03-18
*	Rename subst_raw_with_bindings to subst_glob_with_bindings and export	msozeau	2011-02-10
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	An experimental support for open constrs in hints and in "using"	herbelin	2010-10-31
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Improving a few error messages in Ltac interpretation	herbelin	2010-09-11
*	Capitulation wrt "change pat with term": instead of solving the	herbelin	2010-07-30
*	oops. commited files I shouldn't have. reverting on r13341	barras	2010-07-28
*	ported r13340 to trunk	barras	2010-07-28
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fixed a bug introduced in a combination in r12807 and revealed in	herbelin	2010-06-28
*	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin	2010-06-14
*	Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).	herbelin	2010-06-13
*	Made intros_until and onInductionArg a bit stricter and robust	herbelin	2010-06-13
*	Fixed a bug in pretty-printing "induction" and "destruct" due to a	herbelin	2010-06-13
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	term matching in ltac was not coherent with match goal in presence of wildcar...	jforest	2010-05-06
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin	2009-12-30
*	Safer, though ad hoc, approach to re-interpretation of the argument of	herbelin	2009-12-28
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24
*	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin	2009-12-24
*	Moved a bit further the code for pattern interpretation in match goal	herbelin	2009-12-23
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Make usage of Dyn explicit	glondu	2009-10-28
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Relaxed error severity when encountering unknown library objects or tactic	gmelquio	2009-10-06
*	Apply "Declare Implicit Tactic" also to terms interpreted as "open	herbelin	2009-09-27
*	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin	2009-09-26
*	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin	2009-09-20
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17