coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...	herbelin	2001-03-05
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	nouvelle implantation de la reduction	barras	2001-03-01
*	uniformisation avec constr des lieurs dans rawterm/pattern	herbelin	2001-02-14
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin	2001-02-06
*	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin	2001-02-05
*	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin	2001-02-05
*	Reparation reduce_to_mind	mohring	2001-02-01
*	- coqc : option -image	filliatr	2001-02-01
*	Bug localisation des Syntactif Definition	herbelin	2001-01-31
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Prise en compte du let-in dans lookup_*_as_renamed	herbelin	2001-01-30
*	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin	2001-01-24
*	Nouveaux bugs instanciation d'evar par des evar	herbelin	2001-01-19
*	Bug environnement	herbelin	2001-01-11
*	Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...	herbelin	2001-01-04
*	Rattrapage d'erreur pour le Case + Eval Compute in pour Definition	delahaye	2001-01-03
*	Bug de contextes	herbelin	2000-12-26
*	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin	2000-12-26
*	Pattern sera mieux dans Pretyping; relâchement head_pattern_bound	herbelin	2000-12-26
*	Un nom long pour les variables de section qui font classe ou coercion; réorg...	herbelin	2000-12-25
*	Bug vieux Match	herbelin	2000-12-25
*	Bug prédicat	herbelin	2000-12-25
*	Bug prédicat old Case/Match	herbelin	2000-12-20
*	Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...	herbelin	2000-12-20
*	Export fonction testant si un inductive est un record	herbelin	2000-12-19
*	Amélioration message d'erreur mauvais prédicat	herbelin	2000-12-18
*	Debut de nettoyage de Simpl	mohring	2000-12-18
*	Suppression du warning several default clauses	herbelin	2000-12-16
*	Bug env vis à vis du let in	herbelin	2000-12-15
*	Bugs calcul du prédicat des Cases et Case	herbelin	2000-12-15
*	Printer	mohring	2000-12-15
*	Mauvais env donné à new_isevar	herbelin	2000-12-14
*	Oubli test de correction à l'instantiation des evars	herbelin	2000-12-14
*	Mise en page	herbelin	2000-12-14
*	LetIn dans Simpl	mohring	2000-12-14
*	Raffinement erreur Wrong Predicate	herbelin	2000-12-14
*	Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...	herbelin	2000-12-14
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Hint Unfold Local + commentaires	mohring	2000-12-12
*	Debut de reparation de simpl	mohring	2000-12-11
*	Bug Cases en presence d'une absence de clause	herbelin	2000-12-05
*	Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage	herbelin	2000-11-29
*	La table de pré-évaluation des constantes ne doit pas persister au discharge	herbelin	2000-11-27
*	Utilisation de Let In pour les constantes locales, prise en compte des Let In...	herbelin	2000-11-27
*	Branchement du mécanisme d'instantiation des Evar en présence de définitio...	herbelin	2000-11-27
*	Prise en compte des let-in dans les fonctions de réduction pour les tactiques	herbelin	2000-11-27
*	Prise en compte de noms absolus dans la nametab	herbelin	2000-11-26
*	Remplacement de certains sp_of_id par des locate	herbelin	2000-11-26