coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-01-07	Restructuration printer et parser	herbelin
2000-01-07	Renommage command en constr	herbelin
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-15	Les inductifs dans Scheme doivent être des ident d'inductifs	herbelin
1999-12-13	- états fabriqués avec -silent	filliatr
1999-12-13	- méthode load sur les Hints	filliatr
1999-12-13	Poursuite intégration du Cases	herbelin
1999-12-12	modules et coqc	filliatr
1999-12-11	Intégration initiale du Cases	herbelin
1999-12-10	bug: enregistrement de vartab au lieu de csttab	filliatr
1999-12-10	- erreurs Pretype	filliatr