coq - The formal proof system

Age	Commit message (Expand)	Author
2001-01-30	Bug fixed: the case [ id : ?1 -> ?2 \|- ?] was missing in tauto_main	sacerdot
2001-01-29	As an heuristic, now both in tauto and intuition we try to avoid the initial	sacerdot
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-26	On n'évite plus les globaux dans Intro, mais on les évite dans Abstract	herbelin
2000-12-26	Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce der...	herbelin
2000-12-25	Command -> Constr	herbelin
2000-12-25	Retrait du test d'existence "is_global" dans Intro ( fresh_id ) d	herbelin
2000-12-25	Normalisation betaiota du pattern avant enregistrement comme hint (certains d...	herbelin
2000-12-25	Bug confusion existS/sigS	herbelin
2000-12-25	Command -> Constr	herbelin
2000-12-20	Toujours Induction	herbelin
2000-12-20	Toujours Induction	herbelin
2000-12-20	Induction/NewInduction	herbelin
2000-12-19	AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disque	delahaye
2000-12-18	Renommages autour de NewInduction	herbelin
2000-12-15	suppression warning et calcule type dans replace_by_meta dans tous les cas	filliatr
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