coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	coq-bugs #12: probleme de metamap resolu	barras	2001-12-18
*	compat ocaml 3.03	filliatr	2001-12-13
*	GROS COMMIT:	barras	2001-11-05
*	let-in dans Refine	filliatr	2001-09-20
*	Refine sur les CoFix	filliatr	2001-06-25
*	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin	2001-05-25
*	Changement de la structure des points fixes	barras	2001-05-03
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	bug de refine: uncaught exception Array.sub	barras	2001-03-09
*	nouvelle implantation de la reduction	barras	2001-03-01
*	suppression warning et calcule type dans replace_by_meta dans tous les cas	filliatr	2000-12-15