aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
Commit message (Expand)AuthorAge
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* Uniformisation de destApplication en destApp; simplification decompose_appGravatar herbelin2005-02-12
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* *** empty log message ***Gravatar courant2003-06-27
* Simplification case_infoGravatar herbelin2003-06-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Allègement du noyauGravatar herbelin2002-11-18
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Réparation hash_consingGravatar herbelin2002-09-29
* RenoncementGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Ajout isEvarGravatar herbelin2001-11-20
* Ajout quelques fonctions; code mortGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...Gravatar herbelin2001-09-09
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Ajout hashconsing universGravatar herbelin2001-07-03
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* Ajout d'une fonction de remplacement d'un sous-terme par un terme.Gravatar clrenard2001-05-15
* Changement de la structure des points fixesGravatar barras2001-05-03
* interdiction occ positives ET negatives dans PatternGravatar werner2001-04-24
* Suppression de mk_constr qui ne respectait pas l'invariant des applications (...Gravatar herbelin2001-04-15
* entetesGravatar filliatr2001-03-15
* compare_constr independent du groupement des applications.Gravatar barras2001-03-08
* Re-Déplacement extended_rel_listGravatar herbelin2001-03-05
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Changement de subst_metaGravatar mohring2001-02-28
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Ajout global_vars_declGravatar herbelin2001-01-24
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Ajout map_constr_with_full_binders et strong pour SimplGravatar herbelin2000-11-27
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* Introduction constant_path = section_pathGravatar herbelin2000-11-20
* Code mortGravatar herbelin2000-11-10
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Nouveau type rec_declarationGravatar herbelin2000-10-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 19:28:17 +0000