aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2005-12-21Uniformisation: extension de la suppression d'un casts dans collapse_app à l...herbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-12-17Orthographe de 'instantiate'herbelin
2005-12-06j'avais oublie ces deux fichiers.gregoire
2005-12-05correction bug 881.gregoire
2005-12-05changement d'egalite pour le named_context_valgregoire
2005-12-02Changement des named_contextgregoire
2005-11-28parametres inductifsmohring
2005-11-23bug #909: Top n'est cree que si le contexte est videbarras
2005-11-18petites corrections + contournement bug projectionsbarras
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-08Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09herbelin
2005-11-08Nettoyage suite nouvel avertissement Z de ocaml 3.09herbelin
2005-11-02Types inductifs parametriquesmohring
2005-09-09Suppression code inactif et commentaire apparemment incorrect (pour éviter c...herbelin
2005-09-08Simplification message d'anomalieherbelin
2005-08-22argument inutilisé de zip: toujours l'identitéletouzey
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
2005-07-21Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ...herbelin
2005-07-13reactivation de l optim des fermeturesbarras
2005-07-13backtrack modif de knh...barras
2005-07-13*** empty log message ***barras
2005-07-12test du tag de reductionbarras
2005-06-28Correction bug #983herbelin
2005-05-23Bug fix for a bug reported by Roland: the function that detects the constantssacerdot
2005-05-05Bug affichage graphe universherbelin
2005-05-05Code v7 obsoleteherbelin
2005-05-05MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Added map_named_contextherbelin
2005-02-18Moved Indmap and ConstrMap from Libnames to Names for use in Cookingherbelin
2005-02-12Uniformisation de destApplication en destAppherbelin
2005-02-12Uniformisation de destApplication en destApp; simplification decompose_appherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-171. added code to handle the inclusion of inductive types and constructors insacerdot
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
2005-01-05[ Waiting for a keyword to control expansion during functor application ]sacerdot
2005-01-03HUGE COMMITsacerdot
2004-12-07* added subst_evaluable_referencesacerdot
2004-12-06Commentaireherbelin
2004-11-29*** empty log message ***gregoire
2004-11-22Code mortherbelin
2004-11-22compatibility with POWERPCgregoire
2004-11-17bug module with ... + vmbarras
2004-11-17bug module M:=N avec vmbarras
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-12Changement dans les boxed values .gregoire
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:03:36 +0000