coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-03	Make it possible to perform proofs by induction even on non-inductive types,	bertot
2001-03-28	amelioration de la structure des univers	barras
2001-03-22	Problèmes de NewInduction	herbelin
2001-03-15	entetes	filliatr
2001-03-09	bug de refine: uncaught exception Array.sub	barras
2001-03-08	changement comparaison etats	filliatr
2001-03-06	Modification de e_give_exact pour eviter d'echouer sur l'unification	mohring
2001-03-06	eta-expansion	mohring
2001-03-06	EAutod (debug)	filliatr
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-03-01	nouvelle implantation de la reduction	barras
2001-02-28	modif	mohring
2001-02-27	EAuto mixte (largeur puis profondeur)	mohring
2001-02-26	changement message d'erreur Abstract	filliatr
2001-02-26	Eauto version en largeur	mohring
2001-02-26	Abstract: on échoue si le but contient des existentielles	filliatr
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