coq - The formal proof system

Age	Commit message (Expand)	Author
2000-10-01	Disparition du type oper mais nouveau type global_reference	herbelin
2000-10-01	Déplacement 'a reference et binder_kind de Term vers Rawterm	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-09-06	Canonisation de certains noms dans Pretyping, Asterm et Safe_typing	herbelin
2000-09-06	code mort	herbelin
2000-08-20	Bug dans le filtrage des paires, nettoyage	herbelin
2000-08-17	Pattern matching de sous-termes + exceptions dans le lexer	delahaye
2000-07-28	Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...	herbelin
2000-07-26	Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...	herbelin
2000-07-26	bug token "<:" et ":<"	herbelin
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-21	retablissement minicoq (pour Jacek)	filliatr
2000-07-21	Pattern -> parsing	delahaye
2000-07-21	Modifs d'interpretation de patterns + exceptions dans le lexer	delahaye
2000-07-20	portage Refine	filliatr
2000-07-01	Précalcul de la forme canonique des constructeurs et arités pour traiter le...	herbelin
2000-07-01	index devenu list_index échoue maintenant avec Not_found et plus Failure	herbelin
2000-06-29	Renommage mk_unsafe_judgment en get_judgment_of	herbelin
2000-06-21	$BINDER -> BINDER	filliatr
2000-06-21	- $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)	filliatr
2000-06-02	':>' est devenu un seul token	herbelin
2000-06-01	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin
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-31	Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs	herbelin
2000-05-26	Modification messages d'erreurs, possibilité de n'importe quel constr dans l...	herbelin
2000-05-23	Réparation bug d'affichage et affichage des instanciations par des {...}	herbelin
2000-05-22	Commentaires	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-18	Ajout warning si variable existant par ailleurs	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-16	RIEN	herbelin
2000-05-05	ajout interp_sort	herbelin
2000-05-03	diverses modifs pour ocamlweb	filliatr
2000-05-03	suppression de Fw pour les implicites	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-05-02	portage Omega (mais toujours pas Zpower et Zlogarithm)	filliatr
2000-05-02	Problème avec SOPATT	herbelin
2000-05-02	Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'	herbelin
2000-04-30	Suite intégration de constr_pattern	herbelin
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-04-28	portage Omega (code seulement)	filliatr
2000-04-28	portage en ocaml / camlp4 3.00	filliatr