diff --git a/.gitignore b/.gitignore
index 8927ccd8..7f5b32f0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -130,3 +130,5 @@ bootstrap/certicoqc/META
 bootstrap/certicoqchk/META
 bootstrap/certicoqc*/glue.c
 bootstrap/certicoqc*/glue.h
+plugin/.merlin
+_build
\ No newline at end of file
diff --git a/.vscode/CertiCoq.code-workspace b/.vscode/CertiCoq.code-workspace
index 9391c9c3..c5c7712c 100644
--- a/.vscode/CertiCoq.code-workspace
+++ b/.vscode/CertiCoq.code-workspace
@@ -6,6 +6,10 @@
 	],
 	"settings": {
 		"coqtop.binPath": "_opam/bin",
-		"coqtop.args": []
+		"coqtop.args": [],
+		"ocaml.sandbox": {
+			"kind": "opam",
+			"switch": "coq817"
+		}
 	}
 }
diff --git a/benchmarks/certicoq_eval.v b/benchmarks/certicoq_eval.v
new file mode 100644
index 00000000..67900810
--- /dev/null
+++ b/benchmarks/certicoq_eval.v
@@ -0,0 +1,97 @@
+From Equations Require Import Equations.
+From Coq Require Import Uint63 Wf_nat ZArith Lia Arith.
+From CertiCoq Require Import CertiCoq.
+
+(* This warns about uses of primitive operations, but we compile them fine *)
+Set Warnings "-primitive-turned-into-axiom".
+
+
+Definition inspect {A} (a : A) : {b | a = b} :=
+  exist _ a eq_refl.
+Notation " x 'eqn:' H " := (exist _ x H) (at level 20, only parsing).
+
+Section FactPrim.
+  Local Open Scope Z_scope.
+
+  Equations fact (n : int) : int 
+    by wf (Z.to_nat (to_Z n)) lt :=
+  | n with inspect (Uint63.eqb n 0) := 
+    | true eqn:_ => 1
+    | false eqn:heq => n * fact (pred n).
+  Next Obligation.
+    pose proof (to_Z_bounded n).
+    pose proof (to_Z_bounded (pred n)).
+    red.
+    eapply Uint63.eqb_false_spec in heq.
+    rewrite <- Z2Nat.inj_succ.
+    assert (φ (n)%uint63 <> 0). intros hq.
+    pose proof (of_to_Z n). rewrite hq in H1. cbn in H1. congruence.
+    2:lia.
+    rewrite pred_spec in H0 |- *.
+    assert (to_Z n - 1 < wB)%Z. lia.
+    eapply Z2Nat.inj_le. lia. lia.
+    rewrite Z.mod_small. 2:lia. lia.
+  Qed.
+End FactPrim.
+From CertiCoq.Benchmarks Require Import sha256.
+From Coq Require Import String.
+Definition test := "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching."%string.
+
+Definition sha := sha256.SHA_256 (sha256.str_to_bytes test).
+
+Definition sha_fast := sha256.SHA_256' (sha256.str_to_bytes test).
+
+Definition sha_fast_noproofs := let x := sha_fast in tt.
+
+Time Eval vm_compute in sha_fast_noproofs.
+(* Executed in 0.004 sec *)
+
+CertiCoq Eval -time sha_fast_noproofs.
+(* Executed in 0.037175 sec *)
+
+Time CertiCoq Eval sha_fast_noproofs.
+(* Finished transaction in 0.06 sec *)
+
+CertiCoq Eval -time sha_fast_noproofs.
+(* Executed in 0.045 sec *)
+CertiCoq Eval -time sha_fast_noproofs.
+
+
+From CertiCoq.Benchmarks Require Import Color.
+
+Time Eval vm_compute in Color.main.
+
+From CertiCoq.Benchmarks Require Import vs.
+Import VeriStar.
+
+Definition vs_easy :=
+  (fix loop (n : nat) (res : veristar_result) :=
+     match n with
+     | 0%nat =>
+       match res with
+       | Valid => true
+       | _ => false
+       end
+     | S n =>
+       let res := check_entailment example_ent in
+       loop n res
+     end) 100 Valid.
+
+Definition vs_hard :=
+  match vs.main_h with
+  | vs.VeriStar.Valid => true
+  | _ => false
+  end.
+
+(*  
+(* Blows up *) Time Eval vm_compute in vs_easy.
+(* Blows up *) Time Eval vm_compute in vs_hard.
+*)
+
+CertiCoq Eval -time vs_hard.
+(* Executed in 0.06s *)
+CertiCoq Eval -time vs_hard.
+
+CertiCoq Eval -time vs_easy.
+(* Executed in 0.007s *)
+
diff --git a/benchmarks/certicoq_eval_issue.v b/benchmarks/certicoq_eval_issue.v
new file mode 100644
index 00000000..2385a79a
--- /dev/null
+++ b/benchmarks/certicoq_eval_issue.v
@@ -0,0 +1,45 @@
+
+From Coq Require Import List Arith Extraction Lia.
+Notation "( x ; p )" := (exist _ x p).
+Example nth {A} (l : list A) : {n : nat | n < length l} -> A.
+Proof.
+  intros n.
+  induction l as [|l' Hl'].
+  - destruct n as [n Hn].
+    simpl in Hn.
+    apply False_rect.
+    inversion Hn.
+    Set Printing Notations.
+  - destruct n as [n Hn].
+    destruct n as [|n'].
+    + (* 0 *)
+      exact l'.
+    + (* S n' *)
+      apply IHHl'.
+      exists n'.
+      simpl in Hn.
+      apply Nat.succ_lt_mono. apply Hn.
+Defined.
+
+Print nth.
+
+Extraction nth.
+
+From CertiCoq.Plugin Require Import CertiCoq.
+
+Import ListNotations.
+Definition l : list nat := map (fun x => x * x) (repeat 3 45000).
+
+Lemma nth_l : 30000 < length l.
+Proof. unfold l. rewrite map_length. rewrite repeat_length. Admitted.
+
+Definition test : nat := (nth l (30000; nth_l)).
+(* Time Eval vm_compute in test. *)
+(* 30 seconds, includes cost of building the intermediate n < length proofs  *)
+(* Stack overflowing? *)
+(* CertiCoq Eval -debug -time test. *)
+Definition largenat := 45000.
+(* Stack overflowing? *)
+
+Definition llength := length l.
+CertiCoq Eval -debug -time llength.
diff --git a/benchmarks/test_primfloat.v b/benchmarks/test_primfloat.v
index d1c64539..bfd6023a 100644
--- a/benchmarks/test_primfloat.v
+++ b/benchmarks/test_primfloat.v
@@ -1,6 +1,6 @@
 
 From CertiCoq.Plugin Require Import CertiCoq.
-From MetaCoq Require Import utils.
+From MetaCoq.Utils Require Import utils.
 From CertiCoq.Common Require Import Pipeline_utils.
 
 Open Scope bs_scope.
@@ -14,7 +14,7 @@ Definition string_of_bool b :=
 #[export] Instance bool_show : Show bool := string_of_bool.
 
 #[export] Instance list_show {A} {SA : Show A} : Show (list A) := string_of_list show.
-From MetaCoq Require Import Primitive.
+From MetaCoq.Common Require Import Primitive.
 From Coq Require Import PrimFloat PrimInt63.
 #[export] Instance float_show : Show PrimFloat.float := string_of_float.
 #[export] Instance prim_int_show : Show PrimInt63.int := string_of_prim_int.
@@ -39,4 +39,6 @@ Definition certicoqc2 :=
   coq_msg_info (show (0%float == (-0)%float)).
 
 Time Eval compute in certicoqc2.
+
+Set Warnings "-primitive-turned-into-axiom".
 Time CertiCoq Run certicoqc2.
\ No newline at end of file
diff --git a/benchmarks/test_primitive.v b/benchmarks/test_primitive.v
index fb63bd20..1450347b 100644
--- a/benchmarks/test_primitive.v
+++ b/benchmarks/test_primitive.v
@@ -1,4 +1,5 @@
-From MetaCoq Require Import bytestring MCString Primitive.
+From MetaCoq.Utils Require Import bytestring MCString. 
+From MetaCoq.Common Require Import Primitive.
 From CertiCoq.Plugin Require Import CertiCoq.
 From Coq Require Import Uint63 ZArith.
 Open Scope bs.
diff --git a/cplugin/_CoqProject b/cplugin/_CoqProject
index 7e557737..382a2724 100644
--- a/cplugin/_CoqProject
+++ b/cplugin/_CoqProject
@@ -468,5 +468,3 @@ extraction/zbool.ml
 extraction/zbool.mli
 extraction/zpower.ml
 extraction/zpower.mli
-extraction/optionMonad.mli
-extraction/optionMonad.ml
diff --git a/cplugin/certicoq.ml b/cplugin/certicoq.ml
index 1ab88c3f..859c5546 100644
--- a/cplugin/certicoq.ml
+++ b/cplugin/certicoq.ml
@@ -280,8 +280,9 @@ let make_pipeline_options (opts : options) =
   let dev = coq_nat_of_int opts.dev in
   let prefix = bytestring_of_string opts.prefix in
   let prims = get_global_prims () @ opts.prims in
+  let name = bytestring_of_string "body" in
   (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *)
-  Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix prims
+  Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix name prims
 
 
 (** Main Compilation Functions *)
diff --git a/plugin/CoqMsgFFI.v b/plugin/CoqMsgFFI.v
index 445a02c8..e246416d 100644
--- a/plugin/CoqMsgFFI.v
+++ b/plugin/CoqMsgFFI.v
@@ -11,4 +11,4 @@ CertiCoq Register [
   coq_msg_notice => "coq_msg_notice",
   coq_msg_debug => "coq_msg_debug",
   coq_user_error => "coq_user_error" ]
-Include [ "coq_c_ffi.h" as library ].
+Include [ "coq_ffi.h" as library ].
diff --git a/plugin/Makefile.local b/plugin/Makefile.local
index 70c4d4ce..1b4fec03 100644
--- a/plugin/Makefile.local
+++ b/plugin/Makefile.local
@@ -8,8 +8,16 @@ CAMLFLAGS+=-w -39 # Unused rec flagss
 CAMLFLAGS+=-w -20 # Unused arguments
 CAMLFLAGS+=-w -60 # Unused functor arguments
 CAMLFLAGS+=-w -8 # Non-exhaustive matches produced by extraction
+CAMLFLAGS+=-w -37 # Unused constructor
 
 CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims
 
+CC=$(shell which gcc || which clang-11)
+
 merlin-hook::
-		$(HIDE)echo 'FLG $(OPENS)' >> .merlin
\ No newline at end of file
+		$(HIDE)echo 'FLG $(OPENS)' >> .merlin
+
+get_ordinal.o: get_ordinal.c
+	$(CC) -c -o $@ -I runtime $<
+
+certicoq_plugin.cmxs: get_ordinal.o
\ No newline at end of file
diff --git a/plugin/Makefile.local-late b/plugin/Makefile.local-late
new file mode 100644
index 00000000..6c6f7343
--- /dev/null
+++ b/plugin/Makefile.local-late
@@ -0,0 +1,4 @@
+# CAMLOPTLINK = "$(OCAMLFIND)" opt      -linkall get_ordinal.o
+
+certicoq_plugin.cmxa: certicoq_plugin.cmx
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $<
diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml
index 8ab0fba1..fabd6ca5 100644
--- a/plugin/certicoq.ml
+++ b/plugin/certicoq.ml
@@ -3,16 +3,52 @@
 (* Copyright (c) 2017                                                 *)
 (**********************************************************************)
 
-open Pp
 open Printer
 open Metacoq_template_plugin.Ast_quoter
 open ExceptionMonad
 open AstCommon
 open Plugin_utils
 
+let get_build_dir_opt =
+  Goptions.declare_stringopt_option_and_ref
+    ~key:["CertiCoq"; "Build"; "Directory"]
+    ~depr:false
+
+(* Taken from Coq's increment_subscript, but works on strings rather than idents *)
+let increment_subscript id =
+  let len = String.length id in
+  let rec add carrypos =
+    let c = id.[carrypos] in
+    if Util.is_digit c then
+      if Int.equal (Char.code c) (Char.code '9') then begin
+        assert (carrypos>0);
+        add (carrypos-1)
+      end
+      else begin
+        let newid = Bytes.of_string id in
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+        Bytes.set newid carrypos (Char.chr (Char.code c + 1));
+        newid
+      end
+    else begin
+      let newid = Bytes.of_string (id^"0") in
+      if carrypos < len-1 then begin
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+        Bytes.set newid (carrypos+1) '1'
+      end;
+      newid
+    end
+  in String.of_bytes (add (len-1))
+
+let debug_reify = CDebug.create ~name:"certicoq-reify" ()
+
+external get_unboxed_ordinal : Obj.t -> int = "get_unboxed_ordinal" [@@noalloc]
+
+external get_boxed_ordinal : Obj.t -> (int [@untagged]) = "get_boxed_ordinal" "get_boxed_ordinal" [@@noalloc]
+
 (** Various Utils *)
 
-let pr_string s = str (Caml_bytestring.caml_string_of_bytestring s)
+let pr_string s = Pp.str (Caml_bytestring.caml_string_of_bytestring s)
 
 (* remove duplicates but preserve order, keep the leftmost element *)
 let nub (xs : 'a list) : 'a list = 
@@ -25,7 +61,7 @@ let rec coq_nat_of_int x =
 
 let debug_msg (flag : bool) (s : string) =
   if flag then
-    Feedback.msg_debug (str s)
+    Feedback.msg_debug (Pp.str s)
   else ()
 
 (* Separate registration of primitive extraction *)
@@ -58,6 +94,63 @@ let register (prims : prim list) (imports : import list) : unit =
 let get_global_prims () = fst !global_registers
 let get_global_includes () = snd !global_registers
 
+(* Support for dynamically-linked certicoq-compiled programs *)
+type certicoq_run_function = unit -> Obj.t
+
+let certicoq_run_functions = 
+  Summary.ref ~name:"CertiCoq Run Functions Table" 
+    (CString.Map.empty : certicoq_run_function CString.Map.t)
+
+let certicoq_run_functions_name = "certicoq-run-functions-registration"
+
+let all_run_functions = ref CString.Set.empty
+
+let cache_certicoq_run_function (s, fn) =
+  let fns = !certicoq_run_functions in
+  all_run_functions := CString.Set.add s !all_run_functions;
+  certicoq_run_functions := CString.Map.add s fn fns
+
+let certicoq_run_function_input = 
+  let open Libobject in 
+  declare_object 
+    (global_object_nodischarge certicoq_run_functions_name
+    ~cache:(fun r -> cache_certicoq_run_function r)
+    ~subst:None)
+
+let register_certicoq_run s fn =
+  Feedback.msg_debug Pp.(str"Registering function " ++ str s ++ str " in certicoq_run");
+  Lib.add_leaf (certicoq_run_function_input (s, fn))
+
+let exists_certicoq_run s =
+  CString.Map.find_opt s !certicoq_run_functions
+
+let run_certicoq_run s = 
+  try CString.Map.find s !certicoq_run_functions
+  with Not_found -> CErrors.user_err Pp.(str"Could not find certicoq run function associated to " ++ str s)
+
+(** Coq FFI: message channels and raising user errors. *)
+
+let coq_msg_info s =
+  let s = Caml_bytestring.caml_string_of_bytestring s in
+  Feedback.msg_info (Pp.str s)
+  
+let _ = Callback.register "coq_msg_info" coq_msg_info
+
+let coq_msg_debug s = 
+  Feedback.msg_debug Pp.(str (Caml_bytestring.caml_string_of_bytestring s))
+  
+let _ = Callback.register "coq_msg_debug" coq_msg_debug
+
+let coq_msg_notice s = 
+  Feedback.msg_notice Pp.(str (Caml_bytestring.caml_string_of_bytestring s))
+  
+let _ = Callback.register "coq_msg_notice" coq_msg_notice
+  
+let coq_user_error s =
+  CErrors.user_err Pp.(str (Caml_bytestring.caml_string_of_bytestring s))
+
+let _ = Callback.register "coq_user_error" coq_user_error 
+
 (** Compilation Command Arguments *)
 
 type command_args =
@@ -73,6 +166,7 @@ type command_args =
  | EXT of string (* Filename extension to be appended to the file name *)
  | DEV of int    (* For development purposes *)
  | PREFIX of string (* Prefix to add to the generated FFI fns, avoids clashes with C fns *)
+ | TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *)
  | FILENAME of string (* Name of the generated file *)
 
 type options =
@@ -89,10 +183,22 @@ type options =
     ext       : string;
     dev       : int;
     prefix    : string;
+    toplevel_name : string;
     prims     : ((Kernames.kername * Kernames.ident) * bool) list;
   }
 
-let default_options : options =
+let check_build_dir d =
+  if d = "" then "." else
+  let isdir = 
+    try Unix.((stat d).st_kind = S_DIR)
+    with Unix.Unix_error (Unix.ENOENT, _, _) ->
+      CErrors.user_err Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.")
+  in
+  if not isdir then 
+    CErrors.user_err Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.")
+  else d
+  
+let default_options () : options =
   { bypass_qed = false;
     cps       = false;
     time      = false;
@@ -101,27 +207,15 @@ let default_options : options =
     debug     = false;
     args      = 5;
     anf_conf  = 0;
-    build_dir = ".";
+    build_dir = (match get_build_dir_opt () with None -> "." | Some s -> check_build_dir s);
     filename  = "";
     ext       = "";
     dev       = 0;
     prefix    = "";
+    toplevel_name = "body";
     prims     = [];
   }
 
-let check_build_dir d =
-  if d = "" then "." else
-  let isdir = 
-    try Unix.((stat d).st_kind = S_DIR)
-    with Unix.Unix_error (Unix.ENOENT, _, _) ->
-      CErrors.user_err ~hdr:"pipeline" 
-        Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.")
-  in
-  if not isdir then 
-    CErrors.user_err ~hdr:"pipeline"
-      Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.")
-  else d
-
 let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ident) * bool) list) (fname : string) : options =
   let rec aux (o : options) l =
     match l with
@@ -140,9 +234,10 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide
     | EXT s    :: xs -> aux {o with ext = s} xs
     | DEV n    :: xs -> aux {o with dev = n} xs
     | PREFIX s :: xs -> aux {o with prefix = s} xs
+    | TOPLEVEL_NAME s :: xs -> aux {o with toplevel_name = s} xs
     | FILENAME s :: xs -> aux {o with filename = s} xs
   in
-  let opts = { default_options with filename = fname } in
+  let opts = { (default_options ()) with filename = fname } in
   let o = aux opts l in
   {o with prims = pr}
 
@@ -156,9 +251,10 @@ let make_pipeline_options (opts : options) =
   let anfc = coq_nat_of_int opts.anf_conf in
   let dev = coq_nat_of_int opts.dev in
   let prefix = bytestring_of_string opts.prefix in
+  let toplevel_name = bytestring_of_string opts.toplevel_name in
   let prims = get_global_prims () @ opts.prims in
   (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *)
-  Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix prims
+  Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims
 
 (** Main Compilation Functions *)
 
@@ -166,16 +262,13 @@ let make_pipeline_options (opts : options) =
 let get_name (gr : Names.GlobRef.t) : string =
   match gr with
   | Names.GlobRef.ConstRef c -> Names.KerName.to_string (Names.Constant.canonical c)
-  | _ -> CErrors.user_err ~hdr:"template-coq" (Printer.pr_global gr ++ str " is not a constant definition")
+  | _ -> CErrors.user_err Pp.(Printer.pr_global gr ++ str " is not a constant definition")
 
 
 (* Quote Coq term *)
-let quote opts gr =
+let quote_term opts env sigma c =
   let debug = opts.debug in
   let bypass = opts.bypass_qed in
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let sigma, c = Evd.fresh_global env sigma gr in
   debug_msg debug "Quoting";
   let time = Unix.gettimeofday() in
   let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass env sigma (EConstr.to_constr sigma c) in
@@ -183,6 +276,12 @@ let quote opts gr =
   debug_msg debug (Printf.sprintf "Finished quoting in %f s.. compiling to L7." time);
   term
 
+let quote opts gr =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma, c = Evd.fresh_global env sigma gr in
+  quote_term opts env sigma c
+
 (* Compile Quoted term with CertiCoq *)
 
 module type CompilerInterface = sig
@@ -255,13 +354,13 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | (CompM.Err s, dbg) ->
       debug_msg debug "Pipeline debug:";
       debug_msg debug (string_of_bytestring dbg);
-      CErrors.user_err ~hdr:"pipeline" (str "Could not compile: " ++ (pr_string s) ++ str "\n")
+      CErrors.user_err Pp.(str "Could not compile: " ++ (pr_string s) ++ str "\n")
 
 
   (* Generate glue code for the compiled program *)
   let generate_glue (standalone : bool) opts globs =
     if standalone && opts.filename = "" then
-      CErrors.user_err ~hdr:"glue-code" (str "You need to provide a file name with the -file option.")
+      CErrors.user_err Pp.(str "You need to provide a file name with the -file option.")
     else
     let debug = opts.debug in
     let options = make_pipeline_options opts in
@@ -287,7 +386,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let time = (Unix.gettimeofday() -. time) in
       debug_msg debug (Printf.sprintf "Printed glue code to file %s in %f s.." cstr time)
     | CompM.Err s ->
-      CErrors.user_err ~hdr:"glue-code" (str "Could not generate glue code: " ++ pr_string s))
+      CErrors.user_err Pp.(str "Could not generate glue code: " ++ pr_string s))
 
   let compile_only (opts : options) (gr : Names.GlobRef.t) (imports : import list) : unit =
     let term = quote opts gr in
@@ -297,8 +396,8 @@ module CompileFunctor (CI : CompilerInterface) = struct
     let term = quote opts gr in
     generate_glue true opts (Ast0.Env.declarations (fst (Obj.magic term)))
     
-  let compiler_executable debug = 
-    let whichcmd = Unix.open_process_in "which gcc || which clang-11" in
+  let find_executable debug cmd = 
+    let whichcmd = Unix.open_process_in cmd in
     let result = 
       try Stdlib.input_line whichcmd 
       with End_of_file -> ""
@@ -310,6 +409,8 @@ module CompileFunctor (CI : CompilerInterface) = struct
       result
     | _ -> failwith "Compiler not found"
 
+  let compiler_executable debug = find_executable debug "which gcc || which clang-11"
+  
   type line = 
     | EOF
     | Info of string
@@ -349,7 +450,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
     let compiler = compiler_executable debug in
     let rt_dir = runtime_dir () in
     let cmd =
-        Printf.sprintf "%s -Wno-everything -g -I %s -I %s -c -o %s %s" 
+        Printf.sprintf "%s -Wno-everything -O2 -fomit-frame-pointer -g -I %s -I %s -c -o %s %s" 
           compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (name ^ ".o") (name ^ ".c") 
     in
     let importso =
@@ -359,10 +460,10 @@ module CompileFunctor (CI : CompilerInterface) = struct
       in 
       let imports' = List.concat (List.map (fun i -> 
         match i with 
-        | FromAbsolutePath s -> [s]
-        | FromRelativePath s -> [s]
-        | _ -> []) imports) in
-      let l = make_rt_file "certicoq_run_main.o" :: List.map oname imports' in
+        | FromAbsolutePath s -> [oname s]
+        | FromRelativePath s -> [oname s]
+        | FromLibrary s -> [make_rt_file (oname s)]) imports) in
+      let l = make_rt_file "certicoq_run_main.o" :: imports' in
       String.concat " " l
     in
     let gc_stack_o = make_rt_file "gc_stack.o" in
@@ -383,11 +484,282 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str cmd)
     | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n  ++ str" while running " ++ str cmd)
   
+
+  let ocamlfind_executable _debug = 
+    "_opam/bin/ocamlfind"
+    (* find_executable debug "which ocamlfind"  *)
+
+  type reifyable_type =
+  | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list
+  | IsPrimitive of Names.Constant.t * Univ.Instance.t * Constr.t list
+  
+  let type_of_reifyable_type = function
+    | IsInductive (hd, u, args) -> Term.applistc (Constr.mkIndU ((hd, u))) args
+    | IsPrimitive (c, u, args) -> Term.applistc (Constr.mkConstU ((c, u))) args
+  
+  let pr_reifyable_type env sigma ty =
+    Printer.pr_constr_env env sigma (type_of_reifyable_type ty)
+
+  let find_nth_constant n ar =
+    let open Inductiveops in
+    let rec aux i const = 
+      if Array.length ar <= i then raise Not_found
+      else if CList.is_empty ar.(i).cs_args then  (* FIXME lets in constructors *)
+        if const = n then i 
+        else aux (i + 1) (const + 1)
+      else aux (i + 1) const
+    in aux 0 0
+  
+  let find_nth_non_constant n ar =
+    let open Inductiveops in
+    let rec aux i nconst = 
+      if Array.length ar <= i then raise Not_found
+      else if not (CList.is_empty ar.(i).cs_args) then 
+        if nconst = n then i 
+        else aux (i + 1) (nconst + 1)
+      else aux (i + 1) nconst
+    in aux 0 0
+
+  let check_reifyable env sigma ty =
+    (* We might have bound universes though. It's fine! *)
+    try let (hd, u), args = Inductiveops.find_inductive env sigma ty in
+      IsInductive (hd, EConstr.EInstance.kind sigma u, args)
+    with Not_found -> 
+      let hnf = Reductionops.whd_all env sigma ty in
+      let hd, args = EConstr.decompose_app sigma hnf in
+      match EConstr.kind sigma hd with
+      | Const (c, u) when Environ.is_primitive_type env c -> 
+        IsPrimitive (c, EConstr.EInstance.kind sigma u, List.map EConstr.Unsafe.to_constr args)
+      | _ -> CErrors.user_err 
+        Pp.(str"Cannot reify values of non-inductive or non-primitive type: " ++ 
+          Printer.pr_econstr_env env sigma ty)
+
+  let ill_formed env sigma ty =
+    match ty with
+    | IsInductive _ -> 
+      CErrors.anomaly ~label:"certicoq-reify-ill-formed"
+      Pp.(str "Ill-formed inductive value representation in CertiCoq's reification for type " ++
+        pr_reifyable_type env sigma ty)
+    | IsPrimitive _ ->
+      CErrors.anomaly ~label:"certicoq-reify-ill-formed"
+      Pp.(str "Ill-formed primitive value representation in CertiCoq's reification for type " ++
+        pr_reifyable_type env sigma ty)
+
+  (* let ocaml_get_boxed_ordinal v = 
+    (* tag is the header of the object *)
+    let tag = Array.unsafe_get (Obj.magic v : Obj.t array) (-1) in
+    (* We turn it into an ocaml int usable for arithmetic operations *)
+    let tag_int = (Stdlib.Int.shift_left (Obj.magic (Obj.repr tag)) 1) + 1 in
+    Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml tag: %i" (Obj.tag tag)));
+    Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal int: %u" tag_int));
+    Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal ordinal: %u" (tag_int land 255)));
+    tag_int land 255 *)
+
+
+  let time ~(msg:Pp.t) f =
+    let start = Unix.gettimeofday() in
+    let res = f () in
+    let time = Unix.gettimeofday () -. start in
+    Feedback.msg_notice Pp.(msg ++ str (Printf.sprintf " executed in %f sec" time));
+    res
+  
+  let reify env sigma ty v : Constr.t = 
+    let open Declarations in
+    let debug s = debug_reify Pp.(fun () -> str s) in
+    let rec aux ty v =
+    match ty with
+    | IsInductive (hd, u, args) -> 
+      let open Inductive in
+      let open Inductiveops in
+      let spec = lookup_mind_specif env hd in
+      let indfam = make_ind_family ((hd, u), args) in
+      let npars = inductive_params spec in
+      let params, _indices = CList.chop npars args in
+      let cstrs = get_constructors env indfam in
+      if Obj.is_block v then
+        let ord = get_boxed_ordinal v in
+        let () = debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in
+        let coqidx = 
+          try find_nth_non_constant ord cstrs 
+          with Not_found -> ill_formed env sigma ty
+        in
+        let cstr = cstrs.(coqidx) in
+        let ctx = Vars.smash_rel_context cstr.cs_args in
+        let vargs = List.init (List.length ctx) (Obj.field v) in
+        let args' = List.map2 (fun decl v -> 
+          let argty = check_reifyable env sigma 
+          (EConstr.of_constr (Context.Rel.Declaration.get_type decl)) in
+          aux argty v) (List.rev ctx) vargs in
+        Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) (params @ args')
+      else (* Constant constructor *)
+        let ord = (Obj.magic v : int) in
+        let () = debug (Printf.sprintf "Reifying constant constructor: %i" ord) in
+        let coqidx = 
+          try find_nth_constant ord cstrs 
+          with Not_found -> ill_formed env sigma ty 
+        in
+        let () = debug (Printf.sprintf "Reifying constant constructor: %i is %i in Coq" ord coqidx) in
+        Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) params
+    | IsPrimitive (c, u, _args) -> 
+      if Environ.is_array_type env c then 
+        CErrors.user_err Pp.(str "Primitive arrays are not supported yet in CertiCoq reification")
+      else if Environ.is_float64_type env c then
+        Constr.mkFloat (Obj.magic v)
+      else if Environ.is_int63_type env c then
+        Constr.mkInt (Obj.magic v)
+      else CErrors.user_err Pp.(str "Unsupported primitive type in CertiCoq reification")
+    in aux ty v
+
+  let reify opts env sigma tyinfo result =
+    if opts.time then time ~msg:(Pp.str "Reification") (fun () -> reify env sigma tyinfo result)
+    else reify env sigma tyinfo result 
+
+  let template name = 
+    Printf.sprintf "\nvalue %s ()\n { struct thread_info* tinfo = make_tinfo(); return %s_body(tinfo); }\n" name name
+  let template_header name = 
+    Printf.sprintf "#include <gc_stack.h>\nextern value %s ();\n" name
+
+  let write_c_driver opts name = 
+    let fname = make_fname opts (opts.filename ^ ".c") in
+    let fhname = make_fname opts (opts.filename ^ ".h") in
+    let fd = Unix.(openfile fname [O_CREAT; O_APPEND; O_WRONLY] 0o640) in
+    let chan = Unix.out_channel_of_descr fd in
+    output_string chan (template name);
+    flush chan;
+    close_out chan;
+    let chan = open_out fhname in
+    output_string chan (template_header name);
+    flush chan; close_out chan;
+    fname
+  
+  let template_ocaml name = 
+    Printf.sprintf "external %s : unit -> Obj.t = \"%s\"\nlet _ = Certicoq_plugin.Certicoq.register_certicoq_run \"%s\" (Obj.magic %s)" name name name name
+  
+  let write_ocaml_driver opts name = 
+    let fname = make_fname opts (opts.filename ^ "_wrapper.ml") in
+    let chan = open_out fname in
+    output_string chan (template_ocaml name);
+    flush chan; close_out chan; fname
+
+  let certicoq_eval_named opts env sigma id c imports =
+    let prog = quote_term opts env sigma c in
+    let tyinfo = 
+      let ty = Retyping.get_type_of env sigma c in
+      (* assert (Evd.is_empty sigma); *)
+      check_reifyable env sigma ty
+    in
+    let () = compile opts (Obj.magic prog) imports in
+    (* Write wrapping code *)
+    let c_driver = write_c_driver opts id in
+    let ocaml_driver = write_ocaml_driver opts id in      
+    let imports = get_global_includes () @ imports in
+    let debug = opts.debug in
+    let suff = opts.ext in
+    let name = make_fname opts (id ^ suff) in
+    let compiler = compiler_executable debug in
+    let ocamlfind = ocamlfind_executable debug in
+    let rt_dir = runtime_dir () in
+
+    let cmd =
+        Printf.sprintf "%s -Wno-everything -g -I %s -I %s -c -o %s %s" 
+          compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (Filename.remove_extension c_driver ^ ".o") c_driver
+    in
+    let importso =
+      let oname s = 
+        assert (CString.is_suffix ".h" s);
+        String.sub s 0 (String.length s - 2) ^ ".o"
+      in 
+      let imports' = List.concat (List.map (fun i -> 
+        match i with 
+        | FromAbsolutePath s -> [oname s]
+        | FromRelativePath s -> [oname s]
+        | FromLibrary s -> [make_rt_file (oname s)]) imports) in
+      let l = imports' in
+      String.concat " " l
+    in
+    let gc_stack_o = make_rt_file "gc_stack.o" in
+    debug_msg debug (Printf.sprintf "Executing command: %s" cmd);
+    let packages = ["coq-core"; "coq-core.plugins.ltac"; "coq-metacoq-template-ocaml"; 
+      "coq-core.interp"; "coq-core.kernel"; "coq-core.library"] in
+    let pkgs = String.concat "," packages in
+    let dontlink = "str,unix,dynlink,threads,zarith,coq-core,coq-core.plugins.ltac,coq-core.interp" in
+    match Unix.system cmd with
+    | Unix.WEXITED 0 ->
+      let shared_lib = name ^ ".cmxs" in
+      let linkcmd =
+        Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \
+        -I %s -I plugin -o %s %s %s %s %s"
+        ocamlfind dontlink pkgs opts.build_dir shared_lib ocaml_driver gc_stack_o 
+        (make_fname opts opts.filename ^ ".o") importso
+      in
+      debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd);
+      (match Unix.system linkcmd with
+      | Unix.WEXITED 0 ->
+          debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" id);
+          Dynlink.loadfile_private shared_lib;
+          debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" id);
+          let result = 
+            if opts.time then time ~msg:(Pp.str id) (run_certicoq_run id)
+            else run_certicoq_run id ()
+          in
+          debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result");
+          reify opts env sigma tyinfo result
+      | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str linkcmd)
+      | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n))
+    | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str cmd)
+    | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n  ++ str" while running " ++ str cmd)
+
+  let next_string_away_from s bad =
+    let rec name_rec s = if bad s then name_rec (increment_subscript s) else s in
+    name_rec s
+  
+  let find_fresh s map = 
+    Feedback.msg_debug Pp.(str "Looking for fresh " ++ str s ++ str " in " ++ prlist_with_sep spc str (CString.Set.elements map));
+    let freshs = next_string_away_from s (fun s -> CString.Set.mem s map) in
+    Feedback.msg_debug Pp.(str "Found " ++ str freshs);
+    freshs
+    
+  let certicoq_eval opts env sigma c imports =
+    let fresh_name = find_fresh opts.filename !all_run_functions in
+    let opts = { opts with toplevel_name = fresh_name ^ "_body"; filename = fresh_name } in
+    certicoq_eval_named opts env sigma fresh_name c imports
+
+  let run_existing opts env sigma c id run =
+    let tyinfo = 
+      let ty = Retyping.get_type_of env sigma c in        
+      check_reifyable env sigma ty
+    in
+    let result = 
+      if opts.time then time ~msg:Pp.(str"Running " ++ id) run
+      else run ()
+    in
+    debug_msg opts.debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result");
+    reify opts env sigma tyinfo result
+    
+  let certicoq_eval opts env sigma c imports =
+    match exists_certicoq_run opts.filename with
+    | None -> certicoq_eval opts env sigma c imports
+    | Some run -> 
+      debug_msg opts.debug (Printf.sprintf "Retrieved earlier compiled code for %s" opts.filename);
+      run_existing opts env sigma c (Pp.str opts.filename) run
+
+  let compile_shared_C opts gr imports =
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let sigma, c = Evd.fresh_global env sigma gr in
+    let name = Names.Id.to_string (Nametab.basename_of_global gr) in
+    match exists_certicoq_run name with
+    | None ->
+      let opts = { opts with toplevel_name = name ^ "_body"; } in
+      certicoq_eval_named opts env sigma name c imports
+    | Some run -> run_existing opts env sigma c (Pp.str name) run
+    
   let print_to_file (s : string) (file : string) =
     let f = open_out file in
     Printf.fprintf f "%s\n" s;
     close_out f
 
+
   let show_ir opts gr =
     let term = quote opts gr in
     let debug = opts.debug in
@@ -408,7 +780,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | (CompM.Err s, dbg) ->
       debug_msg debug "Pipeline debug:";
       debug_msg debug (string_of_bytestring dbg);
-      CErrors.user_err ~hdr:"show-ir" (str "Could not compile: " ++ (pr_string s) ++ str "\n")
+      CErrors.user_err Pp.(str "Could not compile: " ++ (pr_string s) ++ str "\n")
 
 
   (* Quote Coq inductive type *)
@@ -421,8 +793,8 @@ module CompileFunctor (CI : CompilerInterface) = struct
       | Names.GlobRef.IndRef i -> 
           let (mut, _) = i in
           Names.KerName.to_string (Names.MutInd.canonical mut)
-      | _ -> CErrors.user_err ~hdr:"template-coq"
-        (Printer.pr_global gr ++ str " is not an inductive type") in
+      | _ -> CErrors.user_err
+        Pp.(Printer.pr_global gr ++ str " is not an inductive type") in
     debug_msg debug "Quoting";
     let time = Unix.gettimeofday() in
     let term = quote_term_rec ~bypass:true env sigma (EConstr.to_constr sigma c) in
@@ -452,7 +824,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let time = (Unix.gettimeofday() -. time) in
       debug_msg debug (Printf.sprintf "Printed FFI glue code to file in %f s.." time)
     | CompM.Err s ->
-      CErrors.user_err ~hdr:"ffi-glue-code" (str "Could not generate FFI glue code: " ++ pr_string s))
+      CErrors.user_err Pp.(str "Could not generate FFI glue code: " ++ pr_string s))
 
   let glue_command opts grs =
     let terms = grs |> List.rev
diff --git a/plugin/certicoq.mli b/plugin/certicoq.mli
index 68bdae6c..494c98b0 100644
--- a/plugin/certicoq.mli
+++ b/plugin/certicoq.mli
@@ -13,6 +13,7 @@ type command_args =
  | EXT of string (* Filename extension to be appended to the file name *)
  | DEV of int
  | PREFIX of string (* Prefix to add to the generated FFI fns, avoids clashes with C fns *)
+| TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *)
  | FILENAME of string (* Name of the generated file *)
 
 type options =
@@ -29,12 +30,13 @@ type options =
     ext       : string;
     dev       : int;
     prefix    : string;
+    toplevel_name : string;
     prims     : ((Kernames.kername * Kernames.ident) * bool) list;
   }
 
 type prim = ((Kernames.kername * Kernames.ident) * bool)
 
-val default_options : options
+val default_options : unit -> options
 val make_options : command_args list -> prim list -> string -> options
 
 (* Register primitive operations and associated include file *)
@@ -67,6 +69,14 @@ end
 val compile_only : options -> Names.GlobRef.t -> import list -> unit
 val generate_glue_only : options -> Names.GlobRef.t -> unit
 val compile_C : options -> Names.GlobRef.t -> import list -> unit
+val compile_shared_C : options -> Names.GlobRef.t -> import list -> Constr.t
 val show_ir : options -> Names.GlobRef.t -> unit
 val ffi_command : options -> Names.GlobRef.t -> unit
 val glue_command : options -> Names.GlobRef.t list -> unit
+val certicoq_eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t
+
+(* Support for running dynamically linked certicoq-compiled programs *)
+type certicoq_run_function = unit -> Obj.t
+
+val register_certicoq_run : string -> certicoq_run_function -> unit
+val run_certicoq_run : string -> certicoq_run_function
diff --git a/plugin/g_certicoq.mlg b/plugin/g_certicoq.mlg
index 4c7ec4fe..a7e6c9fb 100644
--- a/plugin/g_certicoq.mlg
+++ b/plugin/g_certicoq.mlg
@@ -3,16 +3,46 @@
 DECLARE PLUGIN "coq-certicoq.plugin"
 
 {
+open Names
 open Pp
 open Certicoq
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
 open Plugin_utils
+open Tacexpr
+open Tacinterp
+open Stdarg
+open Tacarg
+open Genredexpr
+
+(** Calling Ltac **)
+
+let ltac_lcall tac args =
+  let (location, name) = Loc.tag (Names.Id.of_string tac)
+    (* Loc.tag @@ Names.Id.of_string tac *)
+  in
+  CAst.make ?loc:location (Tacexpr.TacArg(Tacexpr.TacCall
+                              (CAst.make (Locus.ArgVar (CAst.make ?loc:location name),args))))
+
+
+let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
+  let fold arg (i, vars, lfun) =
+    let id = Names.Id.of_string ("x" ^ string_of_int i) in
+    let (l,n) = (Loc.tag id) in
+    let x = Reference (Locus.ArgVar (CAst.make ?loc:l n)) in
+    (succ i, x :: vars, Id.Map.add id arg lfun)
+  in
+  let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+  let lfun = Id.Map.add (Id.of_string "F") f lfun in
+  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
+  Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
+
+let to_ltac_val c = Tacinterp.Value.of_constr c
 
 }
 
-VERNAC ARGUMENT EXTEND cargs 
+ARGUMENT EXTEND cargs 
 | [ "-bypass_qed" ] -> { BYPASS_QED }
 | [ "-cps" ] -> { CPS }
 | [ "-time" ] -> { TIME }
@@ -26,9 +56,9 @@ VERNAC ARGUMENT EXTEND cargs
 | [ "-dev" natural(n) ] -> { DEV(n) }
 | [ "-ext" string(s) ] -> { EXT(s) }
 | [ "-file" string(s) ] -> { FILENAME(s) }
+| [ "-toplevel_name" string(s) ] -> { TOPLEVEL_NAME(s) }
 END
 
-
 VERNAC ARGUMENT EXTEND extract_cnst 
 | [ reference(gr) "=>" string(str) ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, false) }
 | [ reference(gr) "=>" string(str) "with" "tinfo" ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, true) }
@@ -80,6 +110,18 @@ VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY
   let opts = Certicoq.make_options l [] (get_name gr) in
   Certicoq.compile_C opts gr []
   }
+| [ "CertiCoq" "Eval" cargs_list(l) global(gr) "Extract" "Constants" "[" extract_cnst_list_sep(cs, ",") "]" "Include" "[" cinclude_list_sep(imps, ",") "]" ] -> {
+  let gr = Nametab.global gr in
+  let opts = Certicoq.make_options l cs (get_name gr) in
+  let result = Certicoq.compile_shared_C opts gr imps in 
+  Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result)
+  }
+| [ "CertiCoq" "Eval" cargs_list(l) global(gr) ] -> {
+  let gr = Nametab.global gr in
+  let opts = Certicoq.make_options l [] (get_name gr) in
+  let result = Certicoq.compile_shared_C opts gr [] in
+  Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result)
+  }
 | [ "CertiCoq" "Show" "IR" cargs_list(l) global(gr) ] -> {
     let gr = Nametab.global gr in
     let opts = Certicoq.make_options l [] (get_name gr) in
@@ -104,3 +146,15 @@ VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY
     Feedback.msg_info (str help_msg)
   }
 END
+
+TACTIC EXTEND CertiCoq_eval
+| [ "certicoq_eval" cargs_list(l) constr(c) tactic(tac) ] ->
+  { (* quote and evaluate the given term, unquote, pass the result to t *)
+    Proofview.Goal.enter begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let opts = Certicoq.make_options l [] "goal" in
+      let c' = Certicoq.certicoq_eval opts env sigma c [] in 
+      ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c'])
+  end }
+END
diff --git a/plugin/get_ordinal.c b/plugin/get_ordinal.c
new file mode 100644
index 00000000..b2cdfe5b
--- /dev/null
+++ b/plugin/get_ordinal.c
@@ -0,0 +1,12 @@
+#include "gc_stack.h"
+#include <stdio.h>
+
+value get_unboxed_ordinal(value $v)
+{
+  return Val_long($v);
+}
+
+intnat get_boxed_ordinal(value $v)
+{
+  return *((unsigned long long *) $v + 18446744073709551615LLU) & 255LLU;
+}
diff --git a/plugin/get_ordinal.h b/plugin/get_ordinal.h
new file mode 100644
index 00000000..2e200c67
--- /dev/null
+++ b/plugin/get_ordinal.h
@@ -0,0 +1,4 @@
+#include "values.h"
+
+extern value get_unboxed_ordinal (value);
+extern value get_boxed_ordinal (value);
\ No newline at end of file
diff --git a/plugin/runtime/Makefile b/plugin/runtime/Makefile
index 9626fc49..3446532f 100644
--- a/plugin/runtime/Makefile
+++ b/plugin/runtime/Makefile
@@ -1,17 +1,21 @@
-SRC = gc_stack.c certicoq_run_main.c coq_c_ffi.c prim_int63.c prim_floats.c
-HEADERS = config.h values.h gc_stack.h certicoq_run_main.h coq_c_ffi.h prim_int63.h prim_floats.h
-TARGETS = ${SRC:.c=.o}
+SRC = gc_stack.c certicoq_run_main.c certicoq_run.c coq_c_ffi.c coq_ffi.c prim_int63.c prim_floats.c
+HEADERS = m.h config.h values.h gc_stack.h certicoq_run_main.h certicoq_run.h coq_c_ffi.h coq_ffi.h prim_int63.h prim_floats.h
+LINKOPTS = -linkpkg -dontlink str,unix,dynlink,threads,zarith
 
+TARGETS = ${SRC:.c=.o}
 COQLIB = `coqc -where`
 DST = ${COQLIB}/user-contrib/CertiCoq/Plugin/runtime
 
 all: ${TARGETS}
 
 %.o: %.c
-	gcc -I . -O2 -g -fomit-frame-pointer -c -o $@ $+
+	gcc -I . -I `ocamlc -where` -O2 -g -fomit-frame-pointer -c -o $@ $+
 
 install: all
 	install -d ${DST}
 	install -m 0644 ${HEADERS} ${DST}
 	install -m 0644 ${SRC} ${DST}
 	install -m 0644 ${TARGETS} ${DST}
+	
+clean:
+	rm -f *.o
diff --git a/plugin/runtime/certicoq_run_main.c b/plugin/runtime/certicoq_run_main.c
index 1aecfdcc..3f60ca24 100644
--- a/plugin/runtime/certicoq_run_main.c
+++ b/plugin/runtime/certicoq_run_main.c
@@ -7,10 +7,6 @@ extern void body(struct thread_info *);
 
 extern value args[];
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
-
 int main(int argc, char *argv[]) {
   // value val;
   struct thread_info* tinfo;
diff --git a/plugin/runtime/coq_ffi.c b/plugin/runtime/coq_ffi.c
new file mode 100644
index 00000000..8f6e6757
--- /dev/null
+++ b/plugin/runtime/coq_ffi.c
@@ -0,0 +1,61 @@
+#include <caml/callback.h>
+
+void call_coq_msg_info(value msg)
+{
+  static const value * closure_f = NULL;
+  if (closure_f == NULL) {
+     /* First time around, look up by name */
+    closure_f = caml_named_value("coq_msg_info");
+  }  
+  caml_callback(*closure_f, msg);
+}
+
+value coq_msg_info(value msg) {
+  call_coq_msg_info(msg);
+  return Val_unit;
+}
+
+void call_coq_user_error(value msg)
+{
+  static const value * closure_f = NULL;
+  if (closure_f == NULL) {
+     /* First time around, look up by name */
+    closure_f = caml_named_value("coq_user_error");
+  }
+  caml_callback(*closure_f, msg);
+}
+
+value coq_user_error(value msg) {
+  call_coq_user_error(msg);
+  return Val_unit;
+}
+
+void call_coq_msg_debug(value msg)
+{
+  static const value * closure_f = NULL;
+  if (closure_f == NULL) {
+     /* First time around, look up by name */
+    closure_f = caml_named_value("coq_msg_debug");
+  }
+  caml_callback(*closure_f, msg);
+}
+
+value coq_msg_debug(value msg) {
+  call_coq_msg_debug(msg);
+  return Val_unit;
+}
+
+void call_coq_msg_notice(value msg)
+{
+  static const value * closure_f = NULL;
+  if (closure_f == NULL) {
+     /* First time around, look up by name */
+    closure_f = caml_named_value("coq_msg_notice");
+  }
+  caml_callback(*closure_f, msg);
+}
+
+value coq_msg_notice(value msg) {
+  call_coq_msg_notice(msg);
+  return Val_unit;
+}
diff --git a/plugin/runtime/coq_ffi.h b/plugin/runtime/coq_ffi.h
new file mode 100644
index 00000000..895efe33
--- /dev/null
+++ b/plugin/runtime/coq_ffi.h
@@ -0,0 +1,6 @@
+#include "values.h"
+
+extern value coq_msg_debug(value msg);
+extern value coq_msg_info(value msg);
+extern value coq_msg_notice(value msg);
+extern value coq_user_error(value msg);
diff --git a/plugin/test_certicoq_eval.v b/plugin/test_certicoq_eval.v
new file mode 100644
index 00000000..5d39b82c
--- /dev/null
+++ b/plugin/test_certicoq_eval.v
@@ -0,0 +1,70 @@
+From CertiCoq.Plugin Require Import Loader.
+From CertiCoq.Plugin Require Import CertiCoq.
+From MetaCoq.Utils Require Import utils.
+
+Set CertiCoq Build Directory "_build".
+
+Open Scope bs_scope.
+
+Class Show (A : Type) := show : A -> string.
+
+#[export] Instance nat_show : Show nat := string_of_nat.
+Local Open Scope bs.
+Definition string_of_bool b :=
+  if (b : bool) then "true" else "false".
+#[export] Instance bool_show : Show bool := string_of_bool.
+
+#[export] Instance list_show {A} {SA : Show A} : Show (list A) := string_of_list show.
+From MetaCoq.Common Require Import Primitive.
+From Coq Require Import PrimFloat PrimInt63.
+#[export] Instance float_show : Show PrimFloat.float := string_of_float.
+#[export] Instance prim_int_show : Show PrimInt63.int := string_of_prim_int.
+
+Import SpecFloat.
+Definition string_of_specfloat (f : SpecFloat.spec_float) :=
+  match f with
+  | S754_zero sign => if sign then "-0" else "0"
+  | S754_infinity sign => if sign then "-infinity" else "infinity"
+  | S754_nan => "nan"
+  | S754_finite sign p z => 
+  let num := string_of_positive p ++ "p" ++ string_of_Z z in
+  if sign then "-" ++ num else num
+  end.
+
+#[export] Instance show_specfloat : Show SpecFloat.spec_float := string_of_specfloat.
+#[export] Instance show_positive : Show positive := string_of_positive.
+#[export] Instance show_Z : Show Z := string_of_Z.
+
+Definition certicoqc2 := 5.
+Definition certicoqc3 := coq_msg_notice ("Hello world! " ++ show 100%nat).
+ (* show (0%float == (-0)%float)). *)
+
+Inductive three_ind := One | Two | Three.
+Definition one := One.
+Definition two := Two.
+Definition three := Three.
+
+Definition certicoqc4 :=  (List.map S [26; 20]).
+
+Time Eval compute in certicoqc4.
+Set Warnings "-primitive-turned-into-axiom".
+Set Warnings "backtrace".
+CertiCoq Eval -time -debug certicoqc4. 
+
+Definition largertag := S754_finite true xH 0%Z.
+Definition otherlargertag := S754_infinity true.
+CertiCoq Eval -time -debug otherlargertag.
+
+Set Debug "certicoq-reify".
+Time CertiCoq Eval -time one.
+CertiCoq Eval -time two.
+CertiCoq Eval -time -debug three.
+Time CertiCoq Eval -time -debug three.
+
+(* 
+Goal True.
+  intros.
+  certicoq_eval -build_dir "_build" certicoqc4 ltac:(fun c => assert (certicoqc4 = c) by reflexivity).
+  exact I.
+Qed. *)
+
diff --git a/theories/Codegen/LambdaANF_to_Clight.v b/theories/Codegen/LambdaANF_to_Clight.v
index b7e8ad6b..15099837 100644
--- a/theories/Codegen/LambdaANF_to_Clight.v
+++ b/theories/Codegen/LambdaANF_to_Clight.v
@@ -36,6 +36,7 @@ Variable (limitIdent : ident).
 Variable (gcIdent : ident).
 Variable (mainIdent : ident).
 Variable (bodyIdent : ident).
+Variable (bodyName : string).
 Variable (threadInfIdent : ident).
 Variable (tinfIdent : ident).
 Variable (heapInfIdent : ident).
@@ -1068,7 +1069,7 @@ Fixpoint make_extern_decls
 
 Definition body_external_decl : positive * globdef Clight.fundef type :=
   let params := type_of_params ((tinfIdent, threadInf) :: nil) in
-  (bodyIdent, Gfun (External (EF_external (String.to_string "body")
+  (bodyIdent, Gfun (External (EF_external (String.to_string bodyName)
                                           (signature_of_type  params Tvoid cc_default))
                              params Tvoid cc_default)).
 
@@ -1352,7 +1353,7 @@ Definition add_inf_vars (nenv : name_env) : name_env :=
                   M.set limitIdent (nNamed "limit"%bs) (
                         M.set gcIdent (nNamed "garbage_collect"%bs) (
                                 M.set mainIdent (nNamed "main"%bs) (
-                                       M.set bodyIdent (nNamed "body"%bs) (
+                                       M.set bodyIdent (nNamed bodyName%bs) (
                                                M.set threadInfIdent (nNamed "thread_info"%bs) (
                                                        M.set tinfIdent (nNamed "tinfo"%bs) (
                                                                M.set heapInfIdent (nNamed "heap"%bs) (
diff --git a/theories/Codegen/LambdaANF_to_Clight_stack.v b/theories/Codegen/LambdaANF_to_Clight_stack.v
index c7085e9d..952a4ace 100644
--- a/theories/Codegen/LambdaANF_to_Clight_stack.v
+++ b/theories/Codegen/LambdaANF_to_Clight_stack.v
@@ -43,6 +43,7 @@ Variable (limitIdent : ident).
 Variable (gcIdent : ident).
 Variable (mainIdent : ident).
 Variable (bodyIdent : ident).
+Variable (bodyName : string).
 Variable (threadInfIdent : ident).
 Variable (tinfIdent : ident).
 Variable (heapInfIdent : ident).
@@ -1066,7 +1067,7 @@ Fixpoint make_extern_decls
 
 Definition body_external_decl : positive * globdef Clight.fundef type :=
   let params := type_of_params ((tinfIdent, threadInf) :: nil) in
-  (bodyIdent, Gfun (External (EF_external (String.to_string ("body"%bs))
+  (bodyIdent, Gfun (External (EF_external (String.to_string bodyName)
                                 (signature_of_type  params val cc_default))
                              params val cc_default)).
 
@@ -1266,7 +1267,7 @@ Definition inf_vars :=
   (limitIdent, (nNamed "limit"%bs)) ::
   (gcIdent, (nNamed "garbage_collect"%bs)) ::
   (mainIdent, (nNamed "main"%bs)) ::
-  (bodyIdent, (nNamed "body"%bs)) ::
+  (bodyIdent, (nNamed bodyName)) ::
   (threadInfIdent, (nNamed "thread_info"%bs)) ::
   (tinfIdent, (nNamed "tinfo"%bs)) ::
   (heapInfIdent, (nNamed "heap"%bs)) ::
diff --git a/theories/Codegen/toplevel.v b/theories/Codegen/toplevel.v
index b4f59ccd..46b8d2c0 100644
--- a/theories/Codegen/toplevel.v
+++ b/theories/Codegen/toplevel.v
@@ -38,10 +38,10 @@ Definition add_prim_names (prims : list (kername * string * bool * nat * positiv
   List.fold_left (fun map '(k, s, b, ar, p) => cps.M.set p (nNamed s) map) prims nenv.
 
 
-Definition Clight_trans (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram :=
+Definition Clight_trans (bodyName : string) (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram :=
   let '(_, p_env, cenv, ctag, itag, nenv, fenv, _, prog) := t in
   let p := LambdaANF_to_Clight.compile
-             argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent threadInfIdent
+             argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent bodyName threadInfIdent
              tinfIdent heapInfIdent numArgsIdent isptrIdent caseIdent
              args p_env prog cenv nenv in
   match p with
@@ -52,19 +52,19 @@ Definition Clight_trans (prims : list (kername * string * bool * nat * positive)
 
 
 (* TODO unify with the one above, propagate errors *)
-Definition Clight_trans_fast (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram :=
+Definition Clight_trans_fast (bodyName : string) (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram :=
   let '(_, p_env, cenv, ctag, itag, nenv, fenv, _, prog) := t in
   let '(nenv, prog, head) := LambdaANF_to_Clight.compile_fast
-                               argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent threadInfIdent
+                               argsIdent allocIdent limitIdent gcIdent mainIdent bodyIdent bodyName threadInfIdent
                                tinfIdent heapInfIdent numArgsIdent isptrIdent caseIdent
                                args p_env prog cenv nenv in
   Ret (add_prim_names prims nenv, stripOption mainIdent prog, stripOption mainIdent head).
 
 
-Definition Clight_trans_ANF (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram * string :=
+Definition Clight_trans_ANF bodyName (prims : list (kername * string * bool * nat * positive)) (args : nat) (t : toplevel.LambdaANF_FullTerm) : error Cprogram * string :=
   let '(_, pr_env, cenv, ctag, itag, nenv, fenv, _, prog) := t in
   let '(p, str) := LambdaANF_to_Clight_stack.compile
-                     argsIdent allocIdent nallocIdent limitIdent gcIdent mainIdent bodyIdent threadInfIdent
+                     argsIdent allocIdent nallocIdent limitIdent gcIdent mainIdent bodyIdent bodyName threadInfIdent
                      tinfIdent heapInfIdent numArgsIdent isptrIdent caseIdent resultIdent
                      args
                      pr_env
@@ -85,6 +85,6 @@ Definition compile_Clight (prims : list (kername * string * bool * nat * positiv
     let args := c_args opts in
     let cps := negb (direct opts) in
     if cps then 
-      LiftErrorCertiCoqTrans "Codegen" (Clight_trans prims args) s
+      LiftErrorCertiCoqTrans "Codegen" (Clight_trans opts.(body_name) prims args) s
     else
-      LiftErrorLogCertiCoqTrans "Codegen" (Clight_trans_ANF prims args) s.
+      LiftErrorLogCertiCoqTrans "Codegen" (Clight_trans_ANF opts.(body_name) prims args) s.
diff --git a/theories/Compiler/pipeline.v b/theories/Compiler/pipeline.v
index 761ad7fd..b877e2d3 100644
--- a/theories/Compiler/pipeline.v
+++ b/theories/Compiler/pipeline.v
@@ -143,6 +143,7 @@ Definition default_opts : Options :=
      debug := false;
      dev := 0;
      Pipeline_utils.prefix := "";
+     Pipeline_utils.body_name := "body";
      prims := [];
   |}.
 
@@ -155,6 +156,7 @@ Definition make_opts
            (debug : bool)                            (* Debug log *)
            (dev : nat)                               (* Extra flag for development purposes *)
            (prefix : string)                         (* Prefix for the FFI. Check why is this needed in the pipeline and not just the plugin *)
+           (toplevel_name : string)                  (* Name of the toplevel function ("body" by default) *)
            (prims : list (kername * string * bool))  (* list of extracted constants *)
   : Options :=
   {| direct := negb cps;
@@ -167,6 +169,7 @@ Definition make_opts
      debug := debug;
      dev := dev;
      Pipeline_utils.prefix := prefix;
+     Pipeline_utils.body_name := toplevel_name;
      prims :=  prims |}.
 
 
diff --git a/theories/common/Pipeline_utils.v b/theories/common/Pipeline_utils.v
index 2555cd35..da7a69a6 100644
--- a/theories/common/Pipeline_utils.v
+++ b/theories/common/Pipeline_utils.v
@@ -30,6 +30,7 @@ Record Options :=
     dev      : nat;   (* for development purposes *)
     prefix   : string; (* prefix to generated FFI *)
 
+    body_name : string; (* Name of the toplevel function *)
     prims    : list (kername * string * bool);
     (* List of constants that are realized in the target code.
      * kername: constant name, string: name of target primitive *)