coq - The formal proof system

Age	Commit message (Expand)	Author
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-09-05	Version de la reduction dans Closure plus econome en memoire:	barras
2001-07-21	Nettoyage	herbelin
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin
2001-05-03	Changement de la structure des points fixes	barras
2001-04-15	to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...	herbelin
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-15	entetes	filliatr
2001-03-08	corrections de bug de la reduction	barras
2001-03-01	nouvelle implantation de la reduction	barras
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2000-12-26	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
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