aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-20bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)barras
2004-08-06Amélioration message d'erreur objet de récursion de type non inductifherbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2004-06-02Fusion comparaison Const/Var; export is_opaqueherbelin
2004-05-27Un bug résiduel (mais pas bien méchant) du noyauherbelin
2004-03-28Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...herbelin
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
2003-12-19Inductive Types : seuls les petits types sont unitairesmohring
2003-12-16bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)barras
2003-11-27*** empty log message ***barras
2003-11-25modif lexer: ident peut commencer par _barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:10:06 +0000