aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2006-04-16Nouveau mécanisme pour les modules interactifs : les arguments deherbelin
2006-04-15Inversion de l'ordre de chargement des objets logiques et non logiquesherbelin
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
2006-03-22- Correction bug calcul mind_consnrealargs, introduit à la révisionherbelin
2006-03-18MAJ documentation en syntaxe v8herbelin
2006-03-18Documentation mutual_inductive_bodyherbelin
2006-03-18Bug calcul consnrealargs + bug calcul occurrences non positives + modifs cosm...herbelin
2006-02-16added isProd to term.mli.coq
2006-01-21Variable inutiliséeherbelin
2006-01-20*** empty log message ***barras
2006-01-11Suppression résidus code v7 et traducteurherbelin
2006-01-10Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...herbelin
2006-01-10Détection var inutile par ocaml 3.09herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:06:55 +0000