coq - The formal proof system

Age	Commit message (Expand)	Author
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
1999-10-20	module Clenv (debut)	filliatr