coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Cleaning up the type of Tacinterp.extract_ltac_constr_values.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Monomorphization (tactics)	ppedrot	2012-11-25
*	This patch removes unused "open" (automatically generated from	regisgia	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
*	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
*	Noise for nothing	pboutill	2012-03-02
*	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin	2011-09-26
*	Fixed a problem introduced in r12607 after pattern_of_constr served	herbelin	2010-09-17
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).	herbelin	2010-06-22
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-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
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin	2009-04-24
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	Add a type argument to letin_tac instead of using casts and recomputing	msozeau	2008-09-12
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Instantiation of evars after instantiate (closes #1672).	glondu	2008-02-04
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Suppression de code mort	notin	2007-02-01
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
*	Changement des named_context	gregoire	2005-12-02
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	evar tactic bugfix	corbinea	2004-09-14
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	unification encore...	barras	2004-09-08
*	Protection contre un indice d'evar égal à 0	herbelin	2004-08-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	more evar stuff	corbinea	2004-06-28