coq - The formal proof system

Age	Commit message (Expand)	Author
2002-04-17	Quelques bugs avec inject_nat	herbelin
2002-04-17	jLogic.mli remplace par jolic.mli	herbelin
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2002-04-17	* empty log message *	courant
2002-04-16	Déplacement/renommage de Class.stre_max en Declare.strength_min	herbelin
2002-04-16	Typo	herbelin
2002-04-15	Refine the procedure that generalizes context to current goal.	huang
2002-04-15	integration de coq-inferior par Marco Maggesi	filliatr
2002-04-15	coq-inferior, by Marco Maggesi	filliatr
2002-04-15	maj doc extraction dans repertoire contrib/extraction	letouzey
2002-04-12	backtrack unification	barras
2002-04-12	Intuition	courant
2002-04-12	q: Commande introuvable.	herbelin
2002-04-12	* empty log message *	courant
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