coq - The formal proof system

Age	Commit message (Expand)	Author
2001-09-09	Suppression du retypage dans w_Declare	herbelin
2001-06-29	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-03	Changement de la structure des points fixes	barras
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-03-05	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr
2001-02-28	introduction d'un refine avec resolution des types et de l'instantiation des ...	mohring
2001-01-22	Retour en arrière sur le pb f_equal en attente meilleure solution	herbelin
2001-01-21	Bug « f_equal » : arguments inférables par une unification des types qui n...	herbelin
2000-12-16	Redondant or incompatible instantiations in clenv_assign now correctly trapped	herbelin
2000-12-05	Prise en compte Let dans le calcul des arguments manquants d'un lemme (clenv_...	herbelin
2000-11-27	Branchement du mécanisme d'instantiation des Evar en présence de définitio...	herbelin
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Reparation IsMutConstruct + Transparent	mohring
2000-11-22	Nettoyage	herbelin
2000-11-07	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-27	Chasse au Cast de Cast	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-10-01	Plus de whd_castapp_stack	herbelin
2000-09-26	Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Suppression de Abst	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-06-28	Modifs de presentation.	delahaye
2000-06-21	portage EAuto et Ring	filliatr
2000-05-31	Nettoyage de Generic	herbelin
2000-05-25	Bug existential_value au lieu de existential_type + divers sur existential	herbelin
2000-05-18	bug (typage avec meta)	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-04-28	chgt unify_0	herbelin
2000-04-26	Introduction d'un type constr_pattern pour les différents filtrages	herbelin
2000-03-21	Remplacement plain_instance en instance qui n'a plus besoin de env	herbelin
2000-03-17	Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'	herbelin
1999-12-14	rattrapage exceptions autres que UserError	filliatr
1999-12-14	bug mk_clenv_from lorsque pas d arguments	filliatr
1999-12-13	- états fabriqués avec -silent	filliatr
1999-12-05	premier debugage	filliatr
1999-12-03	- coqmktop	filliatr
1999-12-02	modifs pour premiere edition de liens	filliatr
1999-12-01	- Typing -> Safe_typing	filliatr
1999-11-24	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr
1999-11-22	module Wcclausenv	filliatr
1999-10-20	- documentation repertoire proofs/	filliatr