coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	Revise API of understand_ltac to be parameterized by a flag for resolution of...	msozeau	2012-03-14
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	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
*	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin	2009-12-24
*	Take constraints into account in the "instantiate" tactic	herbelin	2009-10-30
*	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
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Fixes incorrect handling of existing existentials variables in	msozeau	2008-06-03
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...	notin	2007-04-26
*	Report de révision 9583 de la v8.1 dans le trunk	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
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	unification encore...	barras	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	bypass w_Define when w_refine-ing	corbinea	2004-07-07
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	more evar stuff	corbinea	2004-06-28
*	effective evar refining	corbinea	2004-06-26
*	Amélioration du message d'erreur "w_unify"	clrenard	2003-12-01
*	Amelioration du message d'erreur en cas de tentative d'instanciation	clrenard	2003-11-15
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Added Instantiate ... in	corbinea	2003-11-06
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	backtrack dans l'algo d'unification	barras	2002-04-10
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12