coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing bug #4511: evar tactic can create non-typed evars.	Pierre-Marie Pédrot	2016-01-24
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".	Hugo Herbelin	2015-03-07
*	Update headers.	Maxime Dénès	2015-01-12
*	Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...	Hugo Herbelin	2014-11-30
*	Used an evar name based on the local def name in "evar" tactic.	Hugo Herbelin	2014-11-25
*	Merging some functions from evarutil.ml/evd.ml.	Hugo Herbelin	2014-09-29
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Adds an identifier context in pretying's Ltac context.	Arnaud Spiwack	2014-09-05
*	Better structure for Ltac pretyping environments.	Pierre-Marie Pédrot	2014-08-07
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Removing the Change_evar refiner rule.	Pierre-Marie Pédrot	2014-03-31
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	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