coq - The formal proof system

Age	Commit message (Expand)	Author
2002-05-07	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr
2002-05-06	Cosmétique	herbelin
2002-05-06	Standardisation	herbelin
2002-05-06	MAJ	herbelin
2002-05-03	Simplification du filtrage si la premiere ligne de motifs est inevitable + au...	herbelin
2002-05-02	Minor correction of get_lem_name	coq
2002-05-02	nettoyage code	courant
2002-04-24	petit bug dans les noms de fichiers	letouzey
2002-04-19	lemmes sur Zdiv/Zmod	filliatr
2002-04-19	jLogic disparaît	herbelin
2002-04-19	un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...	filliatr
2002-04-18	Suppression d'un warning plus surprenant qu'utile	herbelin
2002-04-18	* empty log message *	letouzey
2002-04-17	* empty log message *	werner
2002-04-17	Ajout remarques diverses et tactiques	herbelin
2002-04-17	typed unification in the case of Pattern	barras
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