coq - The formal proof system

Age	Commit message (Expand)	Author
2000-10-01	Plus de whd_castapp	herbelin
2000-10-01	Plus de whd_castapp_stack	herbelin
2000-09-26	Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Suppression de Abst	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-08-17	Pattern matching de sous-termes	delahaye
2000-07-25	retablissement make doc et make minicoq	filliatr
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclaration...	herbelin
2000-07-21	Pattern -> parsing	delahaye
2000-07-21	Modifs d'interpretation de patterns	delahaye
2000-07-20	portage Refine	filliatr
2000-07-03	Correction de Cofix	delahaye
2000-07-01	Extension de find_inductive aux co-inductifs et renommage en find_rectype	herbelin
2000-06-29	Rien	herbelin
2000-06-28	Modifs de presentation.	delahaye
2000-06-21	portage EAuto et Ring	filliatr
2000-06-01	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin
2000-05-31	Nettoyage de Generic	herbelin
2000-05-25	Déplacement de save_thm and co de PFedit vers Command	herbelin
2000-05-25	Bug existential_value au lieu de existential_type + divers sur existential	herbelin
2000-05-23	Doc	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-18	bug (typage avec meta)	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-18	doc	herbelin
2000-05-16	Retrait du i pour tclTHEN_i et correction bugs Decompose	herbelin
2000-05-05	Achèvement nettoyage Pfedit	herbelin
2000-05-04	Nettoyage de l'interface de Pfedit	herbelin
2000-05-03	compilation bytecode / native :	filliatr
2000-05-03	Completion d'un match non exhaustif	delahaye
2000-05-03	diverses modifs pour ocamlweb	filliatr
2000-05-03	Ajout du langage de tactiques	delahaye
2000-05-02	portage Omega (mais toujours pas Zpower et Zlogarithm)	filliatr
2000-05-02	Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'	herbelin
2000-04-30	Suite intégration de constr_pattern	herbelin
2000-04-28	Renommage bdize -> ast_of_constr	herbelin
2000-04-28	Decoupage de tactics/pattern en proofs/pattern et tactics/hipattern	herbelin
2000-04-28	chgt unify_0	herbelin
2000-04-26	Introduction d'un type constr_pattern pour les différents filtrages	herbelin
2000-04-20	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin
2000-03-28	Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...	herbelin
2000-03-21	Modification de type_of_case, type_case_branches, etc	herbelin
2000-03-21	Remplacement plain_instance en instance qui n'a plus besoin de env	herbelin
2000-03-17	Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'	herbelin
2000-01-28	documentation	filliatr
2000-01-26	MAJ ocaml 2.99 (espaces dans la syntaxe des cast)	herbelin