coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Cosmétique	herbelin	2002-05-06
*	Standardisation	herbelin	2002-05-06
*	MAJ	herbelin	2002-05-06
*	Simplification du filtrage si la premiere ligne de motifs est inevitable + au...	herbelin	2002-05-03
*	Minor correction of get_lem_name	coq	2002-05-02
*	nettoyage code	courant	2002-05-02
*	petit bug dans les noms de fichiers	letouzey	2002-04-24
*	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-19
*	Suppression d'un warning plus surprenant qu'utile	herbelin	2002-04-18
*	* empty log message *	letouzey	2002-04-18
*	* 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-17
*	Déplacement/renommage de Class.stre_max en Declare.strength_min	herbelin	2002-04-16
*	Typo	herbelin	2002-04-16
*	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-15
*	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-12
*	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-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