aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Remove dead code in Environ.Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
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
side_effects. Partial solution to the handling of side effects in proofview.
2016-10-06Removing a slow access to a named environment.Pierre-Marie Pédrot
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
Was PR#263: Fast lookup in named contexts
2016-09-29UPDATE: reference to a deprecated variable "Filename.temp_dir_name" was ↵Matej Kosik
replaced with the recommended "Filename.get_temp_dir_name".
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
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
The greatest danger of OCaml's polymorphic equality is that PMP can replace it with pointer equality at any time, be warned :) The lack of optimization may account for an exponential blow-up in size of the generated code, as well as worse runtime performance.
2016-09-09Removing the now useless field env_named_val from named_context_val.Pierre-Marie Pédrot
This field was only used by the VM before, but since the previous patches, this part of the code relies on the map instead.
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-08Merge PR #244.Pierre-Marie Pédrot
2016-09-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-02Remove useless debug code.Guillaume Melquiond
2016-09-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-01More efficient data structure to check if a native file is loaded.Maxime Dénès
Spotted by PMP.
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function ↵Matej Kosik
composition operator. Short story: This pull-request: (1) removes the definition of the "right-to-left" function composition operator (2) adds the definition of the "left-to-right" function composition operator (3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead. Long story: In mathematics, function composition is traditionally denoted with ∘ operator. Ocaml standard library does not provide analogous operator under any name. Batteries Included provides provides two alternatives: _ % _ and _ %> _ The first operator one corresponds to the classical ∘ operator routinely used in mathematics. I.e.: (f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "right-to-left" composition because: - the function we write as first (f4) will be called as last - and the function write as last (f1) will be called as first. The meaning of the second operator is this: (f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "left-to-right" composition because: - the function we write as first (f1) will be called first - and the function we write as last (f4) will be called last That is, the functions are written in the same order in which we write and read them. I think that it makes sense to prefer the "left-to-right" variant because it enables us to write functions in the same order in which they will be actually called and it thus better fits our culture (we read/write from left to right).
2016-08-26CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, ↵Matej Kosik
which can be useful in general, and then simplifying "Printer.pr_named_decl" function
2016-08-26CLEANUP: rename "Context.Named.{to,of}_rel" functions to ↵Matej Kosik
"Context.Named.{to,of}_rel_decl"
2016-08-26CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Matej Kosik
2016-08-25Merge remote-tracking branch 'v8.6' into trunkMatej Kosik
2016-08-25CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeMatej Kosik
2016-08-25CLEANUP: Type alias "Context.section_context" was removedMatej Kosik
2016-08-25CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵Matej Kosik
"Context.{Rel,Named}.fold_constr"
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called.
2016-08-24Changing the definition of the "Lib.variable.info" type to enable us to do ↵Matej Kosik
more cleanups
2016-08-24Merging a branch that adds "Context.Named.Declaration.to_rel" function.Matej Kosik
2016-08-24Adding "Context.Named.Declaration.to_rel" functionMatej Kosik
2016-08-22Use a better data structure for VM compilation of free vars.Pierre-Marie Pédrot
This fixes #3450 and probably provides a huge speed-up to many instances.
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
Suggested by @ppedrot
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
2016-08-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-17Revert "CLEANUP: removing the definition of the ↵Pierre-Marie Pédrot
"Context.Rel.Declaration.to_tuple" function" This reverts commit 4b24bb7d3b770592015c264001b9aed9fe95c200. While the of_tuple function is clearly dubious and mostly used for compatiblity reasons, and thus had to be removed, I think that the to_tuple function is still useful as it allows to access each component of the declaration piecewise. Without it, some codes tend to get cluttered with useless projections here and there.
2016-08-11Adding "Context.Named.Declaraton.of_rel" functionMatej Kosik
2016-08-11CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" ↵Matej Kosik
function
2016-08-11CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" ↵Matej Kosik
function
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
In coqtop, one could do for instance: Require Import Top. (* Where Top contains a Definition b := true *) Lemma bE : b = true. Proof. reflexivity. Qed. Definition b := false. Lemma bad : False. Proof. generalize bE; compute; discriminate. Qed. That proof could however not be saved because of the circular dependency check. Safe_typing now checks that we are not requiring (Safe_typing.import) a library with the same logical name as the current one.
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 00:11:34 +0000