coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fix for bug #2350 was really too quick. Here is a version that works better.	herbelin	2010-07-21
*	Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).	herbelin	2010-07-21
*	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
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Clarification in comments	glondu	2009-10-28
*	fixed czar bug with parametric inductives	corbinea	2009-10-27
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin	2009-06-06
*	## Lines starting with '## ' will be removed from the log message.	msozeau	2009-06-01
*	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin	2009-04-08
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	About "apply in":	herbelin	2008-12-09
*	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin	2008-11-04
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Backtrack sur l'effacement dans le contexte de but des lieurs	herbelin	2007-05-19
*	Wish #1582 (3eme)	herbelin	2007-05-18
*	Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)	herbelin	2007-05-18
*	Quelques essais autour du wish implicite au rapport de bug #1582	herbelin	2007-05-18
*	Correction d'un bug refine	herbelin	2006-11-10
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	Garder les cast semble décidément le meilleur moyen de rester synchrone ave...	herbelin	2004-12-06
*	Suppression des cast après avoir utiliser l'information de type (Tacinv envo...	herbelin	2004-12-06
*	Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch...	herbelin	2004-12-06
*	Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ...	herbelin	2004-12-06
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	Nouvelle en-tête	herbelin	2004-07-16
*	bug #787 de Roland	barras	2004-06-02
*	Correction bug soumis par Yves	herbelin	2003-12-13
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
*	Simplification de Proof_type.prim_rule	herbelin	2002-03-27
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15