coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-03-20	Affichage des anonymes si lambda	herbelin
2000-03-07	Capture des exceptions si env vide pour ne pas echouer lors du debogage	herbelin
2000-01-31	Export gentermpr avec renommage	herbelin
2000-01-26	MAJ ocaml 2.99 (espaces dans la syntaxe des cast)	herbelin
2000-01-26	Fin du changement comarg -> constrarg	herbelin
2000-01-26	Abstraction de l'implémentation des signatures de Sign en vue intégration d...	herbelin
2000-01-21	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr
2000-01-20	Bête renommage	herbelin
2000-01-13	Nettoyage des fichiers de parsing	herbelin
2000-01-11	Ajout '\|' en tete de filtrage	herbelin
2000-01-07	Grammaire pour Grammar et Syntax, avant dans Extend	herbelin
2000-01-07	MAJ	herbelin
2000-01-07	Renommage command en constr	herbelin