coq - The formal proof system

Age	Commit message (Expand)	Author
2002-05-15	Contournement de la fermeture ML dans VContext	herbelin
2002-05-15	MAJ	herbelin
2002-05-15	MAJ V7.3	herbelin
2002-05-15	maj	filliatr
2002-05-15	mention -dump-glob	filliatr
2002-05-14	MAJ	herbelin
2002-05-14	- Changement de l'ordre de filtrage dans "Match Context"	herbelin
2002-05-14	Utilisation d'une construction spéciale SECVAR pour gérer la	herbelin
2002-05-14	petite erreur de syntaxe	barras
2002-05-14	modification de clenv_merge:	barras
2002-05-14	Ajout de la modification des sortes d'elimination	mohring
2002-05-14	ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite	barras
2002-05-14	Changement de eq en eqT comme equivalence de setoide par defaut.	clrenard
2002-05-14	encore des lemmes sur Zdiv	filliatr
2002-05-14	nouveaux lemmes dans Zdiv (Claude Marche)	filliatr
2002-05-13	Utilisation des de Bruijn pour la constructions des records et de leur projec...	herbelin
2002-05-13	Pas de projection si le nom d'un champ est '_' dans un Record	herbelin
2002-05-10	Plus de souplesse pour les constructeurs encapsulés sous des définitions	herbelin
2002-05-07	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr
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