coq - The formal proof system

Age	Commit message (Expand)	Author
2002-04-12	* empty log message *	herbelin
2002-04-12	Interdiction de nommer une constante comme une variable de section (plus simp...	herbelin
2002-04-12	maj test des reals	letouzey
2002-04-12	petit bug avec dummy_lams	letouzey
2002-04-12	Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannion	herbelin
2002-04-11	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin
2002-04-11	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin
2002-04-10	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-08	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-05	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-04	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-03	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-02	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-03-29	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-28	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-27	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-26	Refonte complete de la génération des types ML	letouzey