coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin	2002-04-11
*	Simplification du nom de l'architecture Mac OS X	herbelin	2002-04-10
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	backtrack dans l'algo d'unification	barras	2002-04-10
*	Syntactic Definition autorisée dans les motifs de Cases (utile notamment	herbelin	2002-04-10
*	MAJ	herbelin	2002-04-10
*	Simplification des Clear internes dégénérés (sans hypothèses à effacer)	herbelin	2002-04-10
*	MAJ	herbelin	2002-04-10
*	package camlindent inutilise	barras	2002-04-10
*	extraction.ml	letouzey	2002-04-08
*	babioles de renommages	letouzey	2002-04-08
*	Zdiv -> Export ZArith	filliatr	2002-04-08
*	syntaxe pour Zdiv et Zmod	filliatr	2002-04-08
*	ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...	letouzey	2002-04-08
*	* empty log message *	courant	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
*	simplification preuve	filliatr	2002-04-05
*	nouveau module Zdiv	filliatr	2002-04-05
*	mise jour	filliatr	2002-04-05
*	* empty log message *	mohring	2002-04-05
*	meilleure gestion du point terminal	filliatr	2002-04-04
*	resolution du pb d'efficacite du a Sign.add_named_decl	barras	2002-04-04
*	Added credits for jprover.	huang	2002-04-04
*	* empty log message *	huang	2002-04-04
*	Add citations	huang	2002-04-04
*	renommage de l'exception locale Arity	barras	2002-04-03
*	transformation des evar en meta preserve la linearite des metas	barras	2002-04-03
*	changement de l'undo limit	barras	2002-04-03
*	Optimisation	desmettr	2002-04-02
*	Suppression PI_lb et PI_ub	desmettr	2002-04-02
*	Suppression Field	desmettr	2002-04-02
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
*	sans utiliser Field	desmettr	2002-03-29
*	Correction bug infix sur des varaiables	mohring	2002-03-29
*	* empty log message *	mohring	2002-03-29
*	Suppression des invocations a Field	desmettr	2002-03-29
*	reparation du cas des arguments de type qui sont des arités + patch dummy ap...	letouzey	2002-03-28
*	petite erreur dans le typage des let-in	barras	2002-03-28
*	Bug d'affichage des erreurs localisées dans un fichier suite à	herbelin	2002-03-27
*	Simplification de Proof_type.prim_rule	herbelin	2002-03-27
*	Elimination Elimdep.v	mohring	2002-03-27
*	* empty log message *	mohring	2002-03-27
*	Refonte complete de la génération des types ML	letouzey	2002-03-26
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
*	* empty log message *	werner	2002-03-22
*	code redondant	herbelin	2002-03-22
*	Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...	herbelin	2002-03-22
*	An intuitionistic first-order theorem prover -- JProver.	huang	2002-03-22
*	backtrack de l'unification	barras	2002-03-21