coq - The formal proof system

Age	Commit message (Expand)	Author
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-11-06	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-11	Ajout mind_arities_env	herbelin
2000-10-06	Correction incompatibilites dans la fn des types des inductifs	herbelin
2000-09-15	Commentaires	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-07-01	Précalcul de la forme canonique des constructeurs et arités pour traiter le...	herbelin
2000-06-21	bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...	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;Suppression des DLAM en tête des listes de constructeurs	herbelin
2000-05-22	Changement nom module Constant en Declarations	herbelin