coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	pattern-matching avec cas inutilise dans closure	barras	2002-10-15
*	Strengthenning rules for modules + No modules in sections	coq	2002-08-16
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	open Univ inutile	courant	2002-03-12
*	cosmetique	herbelin	2002-01-30
*	compat ocaml 3.03	filliatr	2001-12-13
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	GROS COMMIT:	barras	2001-11-05
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Transparent	barras	2001-09-20
*	Version de la reduction dans Closure plus econome en memoire:	barras	2001-09-05
*	Nettoyage	herbelin	2001-07-21
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
*	Changement de la structure des points fixes	barras	2001-05-03
*	to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...	herbelin	2001-04-15
*	amelioration de la consommation memoire de la conversion en eta-expansant	barras	2001-03-23
*	entetes	filliatr	2001-03-15
*	corrections de bug de la reduction	barras	2001-03-08
*	nouvelle implantation de la reduction	barras	2001-03-01
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin	2000-12-26
*	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin	2000-12-14
*	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-27
*	Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab	filliatr	2000-11-24
*	Ajout d'une fonction pour recuperer la liste des constantes	delahaye	2000-11-21
*	Introduction constant_path = section_path	herbelin	2000-11-20
*	Bug réduction suite modifs let-in	herbelin	2000-10-24
*	La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calcul	herbelin	2000-10-23
*	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin	2000-10-18
*	Renommage canonique :	herbelin	2000-10-18
*	Touche finale à la réduction du let in dans conv et closure	herbelin	2000-10-04
*	Renommage AppL en App	herbelin	2000-10-01
*	Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...	herbelin	2000-09-14
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
*	Suppression de Abst	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
*	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin	2000-05-18
*	- environment -> safe_environment	filliatr	1999-12-01
*	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr	1999-11-24
*	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr	1999-10-18
*	deplacements des var. ex. hors du noyau	filliatr	1999-10-08
*	- abstraction	filliatr	1999-08-26
*	modules Instantiate, Constant et Inductive	filliatr	1999-08-25
*	mach et himsg; typage sans extraction	filliatr	1999-08-24