coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard	2001-11-06
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Suppression du retypage dans w_Declare	herbelin	2001-09-09
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	Bug dans l'utilisation de l'option debug	herbelin	2000-12-20
*	Code mort	herbelin	2000-12-18
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	Renommage canonique :	herbelin	2000-10-18
*	Correction pour make doc	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Nettoyage de Generic	herbelin	2000-05-31
*	Nettoyage de l'interface de Pfedit	herbelin	2000-05-04
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	Suite intégration de constr_pattern	herbelin	2000-04-30
*	MAJ ocaml 2.99 (espaces dans la syntaxe des cast)	herbelin	2000-01-26
*	rattrapage exceptions autres que UserError	filliatr	1999-12-14
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	- Typing -> Safe_typing	filliatr	1999-12-01
*	modules Evar_refiner et Typing_ev	filliatr	1999-10-20