coq - The formal proof system

Age	Commit message (Expand)	Author
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras
2001-10-17	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin
2001-10-12	Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-19	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...	herbelin
2001-09-10	Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...	herbelin
2001-09-09	Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...	herbelin
2001-07-23	Comentaire errone.	clrenard
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin
2001-07-03	Ajout hashconsing univers	herbelin
2001-05-15	Ajout d'une fonction de remplacement d'un sous-terme par un terme.	clrenard
2001-05-03	Changement de la structure des points fixes	barras
2001-04-15	Suppression de mk_constr qui ne respectait pas l'invariant des applications (...	herbelin
2001-04-02	mise a jour pour ocamlweb	filliatr
2001-03-15	entetes	filliatr
2001-03-05	Re-Déplacement extended_rel_list	herbelin
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-01-24	Ajout global_vars_decl	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-11-27	Ajout map_constr_with_full_binders et strong pour Simpl	herbelin
2000-11-20	Introduction constant_path = section_path	herbelin
2000-11-07	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-24	un espace	herbelin
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-11	Nouveau type rec_declaration	herbelin
2000-10-11	Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)	herbelin
2000-10-03	Rebranchement de la tactique Let	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-10-01	Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...	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-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-19	Quelques (i) pour ne pas casser oczmlweb	coq
2000-07-01	Ajout fonctions sur les arités	herbelin
2000-06-29	Ajout make_typed_lazy	herbelin
2000-06-03	Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constr	herbelin
2000-06-02	doc	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-18	Centralisation prod_name and co dans Environ; mkLambda_string dans Term	herbelin
2000-05-05	doc	herbelin