aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Adding a default safe set of kernel typing flags to Declareops.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-06-09newring: fix for hack using evars as integers.Matthieu Sozeau
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-06-02Please never mention .mli-only file in *.mllib (or future *.mlpack)Pierre Letouzey
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Fix potential race condition in vm_compute.Guillaume Melquiond
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2016-05-19native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-27Fixing an incompatility introduced in a404360: kernel conversion wasHugo Herbelin
2016-04-14This is an attempt to clarify terminology in choosing variable namesHugo Herbelin
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-25Remove int64 emulation in bytecode interpreter.Maxime Dénès
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-22Adding eq/compare/hash for syntactic view atHugo Herbelin
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-10Removing OCaml deprecated function names from the Lazy module.Pierre-Marie Pédrot
2016-03-10Hashconsing modules.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime Dénès
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-02-18ADD: Names.Name.is_{anonymous,name}Matej Kosik
2016-02-17CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-16Term: fix a comment (first de Bruijn index is 1)Pierre Letouzey
2016-02-16Renaming variants of Entries.local_entryMatej Kosik
2016-02-15CLEANUP: Simplifying the changes done in "kernel/*"Matej Kosik
2016-02-09REFORMATTING: kernel/context.ml{,i}Matej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-26Fixing bde12b70 about reporting ill-formed constructor.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17Universes algorithm : clarified commentsJacques-Henri Jourdan
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-11COMMENTS: of "Constr.case_info" type were updated.Matej Kosik
2016-01-11COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Matej Kosik
2016-01-08Be more verbose about failure to compile libraries to native code.Guillaume Melquiond
2016-01-07Fix a misleading comment for substn_varsMatthieu Sozeau
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-05Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:13:07 +0000