coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	petit bug dans les noms de fichiers	letouzey	2002-04-24
*	un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...	filliatr	2002-04-19
*	* empty log message *	letouzey	2002-04-18
*	jLogic.mli remplace par jolic.mli	herbelin	2002-04-17
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Refine the procedure that generalizes context to current goal.	huang	2002-04-15
*	maj doc extraction dans repertoire contrib/extraction	letouzey	2002-04-15
*	maj test des reals	letouzey	2002-04-12
*	petit bug avec dummy_lams	letouzey	2002-04-12
*	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin	2002-04-11
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	extraction.ml	letouzey	2002-04-08
*	babioles de renommages	letouzey	2002-04-08
*	ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...	letouzey	2002-04-08
*	export de la fonction Reductionops.find_conclusion pour l'extraction	letouzey	2002-04-08
*	Suppression de l'application de f_equal2 pour "mult" (non inversible);	herbelin	2002-04-05
*	mise jour	filliatr	2002-04-05
*	* empty log message *	huang	2002-04-04
*	Add citations	huang	2002-04-04
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
*	reparation du cas des arguments de type qui sont des arités + patch dummy ap...	letouzey	2002-03-28
*	Simplification de Proof_type.prim_rule	herbelin	2002-03-27
*	Refonte complete de la génération des types ML	letouzey	2002-03-26
*	An intuitionistic first-order theorem prover -- JProver.	huang	2002-03-22
*	reparation du test des reals	letouzey	2002-03-21
*	considerations de pretty-print	letouzey	2002-03-21
*	deux fichiers supplementaires de customisation d'extraction	letouzey	2002-03-21
*	changement du test extraction suite aux modif inining	letouzey	2002-03-21
*	modification de l'auto-inlining	letouzey	2002-03-21
*	renversement du renommage des variables	letouzey	2002-03-20
*	reparation du controle de l'apparition des termes	letouzey	2002-03-20
*	reorganisation des simplifications: letin eta-expansé apres le kill-dummy	letouzey	2002-03-20
*	un peu moins d'eta-expansion autour des Glob	letouzey	2002-03-20
*	bug optimize_fix fait trop tot	letouzey	2002-03-19
*	suite bug Dglob constant	letouzey	2002-03-19
*	bug avec les MLglob vraiment constants	letouzey	2002-03-19
*	travail sur les stratégies de réduction	letouzey	2002-03-19
*	remplacement des deux constants prop/arity par une seule dummy + pretty-print...	letouzey	2002-03-19
*	Fix d'un bug sur le test des inverses	delahaye	2002-03-19
*	Meilleure gestion de la reduction dans Field	delahaye	2002-03-17
*	epsilon	letouzey	2002-03-15
*	un peu de mise a jour de la doc extraction	letouzey	2002-03-15
*	evite les clash avec le type ocaml unit	letouzey	2002-03-15
*	gros commit: principalement ajout des lambdas arity + leur optimisation en te...	letouzey	2002-03-15
*	reparation semi setoid ring	clrenard	2002-03-14
*	Factorisation de la grammaire pour Extraction Language.	letouzey	2002-03-11
*	cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...	letouzey	2002-03-05
*	Big commit extraction:	letouzey	2002-03-04
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
*	Prise en compte des corps de letin dans les hypothèses	herbelin	2002-03-01