coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	reparation du test des reals	letouzey	2002-03-21
*	Décomposition de l'application n-aire en application binaire pour que Patter...	herbelin	2002-03-21
*	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant	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
*	Intuition now takes an (optional) tactic as parameter. This tactic is	courant	2002-03-20
*	encore quelques petites modif de l'unification	barras	2002-03-20
*	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