New IR in VM: Clambda.

This intermediate representation serves two purposes:
1- It is a preliminary step for primitive machine integers, as iterators
will be compiled to Clambda.
2- It makes the VM compilation passes closer to the ones of
native_compute. Once we unifiy the representation of values, we should
be able to factorize the lambda-code generation between the two
compilers, as well as the reification code.

This code was written by Benjamin Grégoire and myself.

1 files changed, 8 insertions, 0 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 35ef4bfa4..ca904d50b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1466,6 +1466,14 @@ let _ =
 let _ =
   declare_bool_option
     { optdepr  = false;
+      optname  = "dumping VM lambda code after compilation";
+      optkey   = ["Dump";"Lambda"];
+      optread  = Flags.get_dump_lambda;
+      optwrite = Flags.set_dump_lambda }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
       optname  = "explicitly parsing implicit arguments";
       optkey   = ["Parsing";"Explicit"];
       optread  = (fun () -> !Constrintern.parsing_explicit);