coq - The formal proof system

Age	Commit message (Expand)	Author
2000-11-27	Faut-il mettre la réduction let-in dans la réduction unfold ?	herbelin
2000-11-27	Utilisation de Let In pour les constantes locales, prise en compte des Let In...	herbelin
2000-11-24	Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab	filliatr
2000-11-21	Ajout d'une fonction pour recuperer la liste des constantes	delahaye
2000-11-20	Introduction constant_path = section_path	herbelin
2000-10-24	Bug réduction suite modifs let-in	herbelin
2000-10-23	La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calcul	herbelin
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-04	Touche finale à la réduction du let in dans conv et closure	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-09-14	Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-10	Suppression de Abst	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
1999-12-01	- environment -> safe_environment	filliatr
1999-11-24	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr
1999-10-18	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr
1999-10-08	deplacements des var. ex. hors du noyau	filliatr
1999-08-26	- abstraction	filliatr
1999-08-25	modules Instantiate, Constant et Inductive	filliatr
1999-08-24	mach et himsg; typage sans extraction	filliatr
1999-08-18	module Reduction (debut)	filliatr
1999-08-17	module Closure	filliatr