aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
2016-10-06Removing a slow access to a named environment.Pierre-Marie Pédrot
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
2016-09-09Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-09-09Restore native compiler optimizations after they were broken by 9e2ee58.Maxime Dénès
2016-09-09Removing the now useless field env_named_val from named_context_val.Pierre-Marie Pédrot
2016-09-09More efficient implementation of map_named_val.Pierre-Marie Pédrot
2016-09-09Fast access environment in CClosure.Pierre-Marie Pédrot
2016-09-09Tentative fast-access named envPierre-Marie Pédrot
2016-09-09Packing the named_context_val in a proper record and marking it private.Pierre-Marie Pédrot
2016-09-02Remove useless debug code.Guillaume Melquiond
2016-09-01More efficient data structure to check if a native file is loaded.Maxime Dénès
2016-08-22Use a better data structure for VM compilation of free vars.Pierre-Marie Pédrot
2016-08-10Make code a bit clearer by removing optional argument.Guillaume Melquiond
2016-07-26Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-25Fix bug #4876: critical bug in guard condition checker.Matthieu Sozeau
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-05Prevent unsafe overwriting of Required modules by toplevel library.Maxime Dénès
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Shrink Proofs/Obligations by default and deprecateMatthieu Sozeau
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-06-20Fix bug #4825: [clear] should not dependency-check hypotheses that come above...Pierre-Marie Pédrot
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Adding a local type-in-type flag in kernel declarations.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:56:58 +0000