coq - The formal proof system

Age	Commit message (Expand)	Author
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	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-14	Bug affichage	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-07	code mort	herbelin
2001-02-06	EqDecide	filliatr
2001-02-05	Ajout d'une heuristique pour les types dependants	delahaye
2001-02-05	Message d'erreur plus explicite pour Tauto	delahaye
2001-02-05	rétablissement nouveau Tauto	filliatr
2001-02-03	Résolution d'un bug de simplification	delahaye
2001-02-01	application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés	filliatr
2001-02-01	oubli de Closure.EvalConstRef	filliatr
2001-02-01	- coqc : option -image	filliatr
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
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