coq - The formal proof system

Age	Commit message (Expand)	Author
2001-03-05	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr
2001-02-28	introduction d'un refine avec resolution des types et de l'instantiation des ...	mohring
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-16	Prise en compte noms longs dans SuperAuto	herbelin
2001-02-14	Obsolète (cf Coqlib)	herbelin
2001-02-08	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr
2001-02-08	exporting traverse_to and mutate: they are used in pcoq.	bertot
2001-02-07	Reparation du pretty-print pour les tactiques	delahaye
2001-02-06	Correction pour les Unfold/Fold dans Cbv	delahaye
2001-02-01	application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés	filliatr
2001-02-01	* empty log message *	mohring
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2001-01-27	make doc	herbelin
2001-01-22	Retour en arrière sur le pb f_equal en attente meilleure solution	herbelin
2001-01-21	Bug « f_equal » : arguments inférables par une unification des types qui n...	herbelin
2001-01-09	Meta Definition + Tactic Definition	delahaye
2001-01-05	Arite cachee de Match Context + Meta Definition	delahaye
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-26	Elimination des coupures	herbelin
2000-12-25	Remplacement de debug en assert	herbelin
2000-12-20	Code mort	herbelin
2000-12-20	Bug dans l'utilisation de l'option debug	herbelin
2000-12-20	Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...	herbelin
2000-12-20	Ajout set_lc	herbelin
2000-12-19	Correction pour les variables abstraites dans les Tactic Definitions	delahaye
2000-12-18	Code mort	herbelin
2000-12-18	Documentation	herbelin
2000-12-16	Redondant or incompatible instantiations in clenv_assign now correctly trapped	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-12	Hint Unfold Local + commentaires	mohring
2000-12-06	Ajout erreur DoesNotOccurIn	herbelin
2000-12-05	Prise en compte Let dans le calcul des arguments manquants d'un lemme (clenv_...	herbelin
2000-12-02	Portage d'AutoRewrite	delahaye
2000-11-28	Elimination du '	delahaye
2000-11-27	Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...	herbelin
2000-11-27	Branchement du mécanisme d'instantiation des Evar en présence de définitio...	herbelin
2000-11-24	certains effets disparaissent a la sortie des sections, d'autres non (selon S...	filliatr
2000-11-23	Correction d'un bug lorsque des Variables sont clearees dans le but courant	delahaye
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Affichage des paths avec des '.', 2eme; prise en compte qualid	herbelin
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Reparation IsMutConstruct + Transparent	mohring
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin
2000-11-22	Nettoyage	herbelin
2000-11-21	Tout est deja traite dans Tacinterp	delahaye
2000-11-21	Traitement du pretty-print des Redexp	delahaye
2000-11-20	Prise en compte noms longs	herbelin
2000-11-15	methode export	filliatr