coq - The formal proof system

Age	Commit message (Expand)	Author
2000-12-14	LetIn dans Simpl	mohring
2000-12-13	Bug Inversion en présence de méta-variables	herbelin
2000-12-13	conflit useInversionLemma	mohring
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-12	Hint Unfold Local + commentaires	mohring
2000-12-12	Reparation Intro sans nom qui ne reduisait pas le but quand celui-ci	mohring
2000-12-06	message d'erreur	herbelin
2000-12-06	Divers bugs LetTac	herbelin
2000-12-04	caractere opaque des constantes repris en compte	filliatr
2000-12-02	Portage d'AutoRewrite	delahaye
2000-11-29	Nouveau long long avec Coq en tête	herbelin
2000-11-28	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin
2000-11-28	Elimination du '	delahaye
2000-11-27	Prise en compte des let-in dans les fonctions de réduction pour les tactiques	herbelin
2000-11-26	Appel des constantes globaux par des noms absolus	herbelin
2000-11-26	Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...	herbelin
2000-11-24	certains effets disparaissent a la sortie des sections, d'autres non (selon S...	filliatr
2000-11-24	Nouveau choix pour l'intros initial	delahaye
2000-11-23	On n'introduit que des produits non dependants	delahaye
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-21	PatternMatchingFailure n'etait pas rattrapee	herbelin
2000-11-21	Bugs make_tuple et existS_pattern	herbelin
2000-11-20	Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...	herbelin
2000-11-20	Utilisation de global_reference dans pattern	herbelin
2000-11-20	Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...	herbelin
2000-11-15	methode export	filliatr
2000-11-10	Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...	herbelin
2000-11-09	Bug et simplification nouvel Induction	herbelin
2000-11-07	Nettoyage Names suite	herbelin
2000-11-07	Changement/extension dans les noms de parseurs de Grammar	herbelin
2000-11-06	Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....	herbelin
2000-11-06	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr
2000-11-03	compilation des fichiers ml4 sans GNUseries	filliatr
2000-11-02	correction Abstract (et make world passe!)	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-31	- simplification Makefile (compilation des fichiers .ml'; pas encore parfait	filliatr
2000-10-31	.old virés (CVS est là pour ca)	filliatr
2000-10-30	Remplacement de Tauto et Intuition	delahaye
2000-10-27	erreur dans intro_gen corrigée	filliatr
2000-10-27	Intro choue si le nom d'hypothse existe au lieu de mettre un avertissement	herbelin
2000-10-27	Ajoute : Ast dans la regle de grammaire	mayero
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-18	Changement parser par défaut dans Syntax	herbelin
2000-10-13	Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...	herbelin
2000-10-11	C'était pas le bon env dans build_term	herbelin
2000-10-11	Prise en compte de Let à certains endroits	herbelin
2000-10-11	Prise en compte de l'env local dans make_apply_entry	herbelin