aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.ml
AgeCommit message (Expand)Author
2003-06-27*** empty log message ***courant
2003-06-10Simplification case_infoherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2002-11-18Allègement du noyauherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-09-29Réparation hash_consingherbelin
2002-08-13Renoncementherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-03-04Nouveau Rewrite-in plus economiquebarras
2001-12-13compat ocaml 3.03filliatr
2001-11-20Ajout isEvarherbelin
2001-11-20Ajout quelques fonctions; code mortherbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...herbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...herbelin
2001-09-09Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...herbelin
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...herbelin
2001-07-03Ajout hashconsing universherbelin
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-15Ajout d'une fonction de remplacement d'un sous-terme par un terme.clrenard
2001-05-03Changement de la structure des points fixesbarras
2001-04-24interdiction occ positives ET negatives dans Patternwerner
2001-04-15Suppression de mk_constr qui ne respectait pas l'invariant des applications (...herbelin
2001-03-15entetesfilliatr
2001-03-08compare_constr independent du groupement des applications.barras
2001-03-05Re-Déplacement extended_rel_listherbelin
2001-03-01nouvelle implantation de la reductionbarras
2001-02-28Changement de subst_metamohring
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-01-24Ajout global_vars_declherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-27Ajout map_constr_with_full_binders et strong pour Simplherbelin
2000-11-23Reparation IsMutConstruct + Transparentmohring
2000-11-20Introduction constant_path = section_pathherbelin
2000-11-10Code mortherbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-11Nouveau type rec_declarationherbelin
2000-10-11Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)herbelin
2000-10-06correction bug univers (dummy_univ)filliatr
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...herbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Suppression de Abstherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:15:17 +0000