coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-04-28	Changement de représentation du contexte des réf dans rawconstr et pattern	herbelin
2000-04-26	Introduction d'un type constr_pattern pour les différents filtrages	herbelin
2000-04-21	discharge des axiomes	filliatr
2000-04-20	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin
2000-03-31	Portage (pour la forme) de minicoq	herbelin
2000-03-30	erreurs lexicales dans les patterns (manquait des espaces)	filliatr
2000-03-30	Réajout globalize_command	herbelin
2000-03-28	Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...	herbelin
2000-03-23	Amélioration d'un message d'erreur	herbelin
2000-03-21	Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...	herbelin