coq - The formal proof system

Age	Commit message (Expand)	Author
2001-02-12	Theoreme opaques	mohring
2001-02-10	All errors were not well reported before. In particular syntax errors were	bertot
2001-02-09	Two pairs of parentheses were missing.	bertot
2001-02-09	option -m (utilisation memoire)	filliatr
2001-02-09	Bug point final dans la syntaxe theorem_body	herbelin
2001-02-09	MAJ	herbelin
2001-02-09	exported several functions that are used in the graphical interface pcoq.	bertot
2001-02-09	changed the design to have command groups executed in a protected manner	bertot
2001-02-09	exported a few functions that are used in graphical interface pcoq.	bertot
2001-02-09	Several pairs of different functions actually had the same name, so	bertot
2001-02-08	modif de la syntax: assoc a droite pour Ring	mayero
2001-02-08	Simplifications	herbelin
2001-02-08	Scratch par defaut si rien n'est specifier dans Add LoadPath	herbelin
2001-02-08	Suppression warning no .coqrc	herbelin
2001-02-08	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr
2001-02-08	modifs mineures	filliatr
2001-02-08	exporting traverse_to and mutate: they are used in pcoq.	bertot
2001-02-08	export a function that can be used to retrieve the context corresponding	bertot
2001-02-07	Meilleure approche du conflit path/freeze/library_root en séquentialisant la...	herbelin
2001-02-07	code mort	herbelin
2001-02-07	Ajout du Match Context	delahaye
2001-02-07	Reparation du pretty-print pour les tactiques	delahaye
2001-02-07	Modif pour les patterns de sous-termes	delahaye
2001-02-07	Probleme synchronisation roots / inputstate	herbelin
2001-02-07	Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir	herbelin
2001-02-07	Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir	herbelin
2001-02-07	Message d'erreur absolute_reference	herbelin
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-02-07	Chgt signature de type_of_existential	herbelin
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-02-06	mise en place extraction	filliatr
2001-02-06	mise a jour	filliatr
2001-02-06	Correction pour les Unfold/Fold dans Cbv	delahaye
2001-02-06	EqDecide	filliatr
2001-02-06	Ajout d'un exemple	delahaye
2001-02-06	MAJ	herbelin
2001-02-06	Ajout d'une commande pour afficher chaque coercion à la demande	herbelin
2001-02-06	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin
2001-02-05	Extension coerce_to_var	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2001-02-05	Meilleur traitement des noms explicites dans la Nametab; Différentation du t...	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2001-02-05	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye
2001-02-05	calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)	filliatr
2001-02-05	D'autres exemples	delahaye
2001-02-05	Pas d'Apply dans Tauto	delahaye
2001-02-05	Ajout d'une heuristique pour les types dependants	delahaye
2001-02-05	Ajout du test de Tauto	delahaye
2001-02-05	Message d'erreur plus explicite pour Tauto	delahaye