diff --git a/ocaml/fstar-lib/FStar_Compiler_Dyn.ml b/ocaml/fstar-lib/FStar_Compiler_Dyn.ml
deleted file mode 100644
index a138a7cd6c2..00000000000
--- a/ocaml/fstar-lib/FStar_Compiler_Dyn.ml
+++ /dev/null
@@ -1,12 +0,0 @@
-type dyn = Obj.t
-[@printer fun fmt _ -> Format.pp_print_string fmt "<dyn>"]
-[@@deriving show]
-
-let dyn_to_yojson _ = `Null
-let dyn_of_yojson _ = failwith "cannot readback"
-
-let mkdyn (x:'a) : dyn =
-    Obj.repr x
-
-let undyn (d:dyn) : 'a =
-    Obj.obj d
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml
index 0372bbf6b21..65f7516bf92 100644
--- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml
+++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml
@@ -52,13 +52,13 @@ let (__proj__Mkiface__item__iface_type_names :
 type extension_sigelt_extractor =
   FStar_Extraction_ML_UEnv.uenv ->
     FStar_Syntax_Syntax.sigelt ->
-      FStar_Compiler_Dyn.dyn ->
+      FStar_Dyn.dyn ->
         (FStar_Extraction_ML_Syntax.mlmodule, Prims.string)
           FStar_Pervasives.either
 type extension_sigelt_iface_extractor =
   FStar_Extraction_ML_UEnv.uenv ->
     FStar_Syntax_Syntax.sigelt ->
-      FStar_Compiler_Dyn.dyn ->
+      FStar_Dyn.dyn ->
         ((FStar_Extraction_ML_UEnv.uenv * iface), Prims.string)
           FStar_Pervasives.either
 type extension_extractor =
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml
index 7c39b9a57f9..c8689773fa7 100644
--- a/ocaml/fstar-lib/generated/FStar_Parser_AST.ml
+++ b/ocaml/fstar-lib/generated/FStar_Parser_AST.ml
@@ -839,18 +839,18 @@ let (__proj__Mkdep_scan_callbacks__item__add_open :
 type to_be_desugared =
   {
   lang_name: Prims.string ;
-  blob: FStar_Compiler_Dyn.dyn ;
+  blob: FStar_Dyn.dyn ;
   idents: FStar_Ident.ident Prims.list ;
-  to_string: FStar_Compiler_Dyn.dyn -> Prims.string ;
-  eq: FStar_Compiler_Dyn.dyn -> FStar_Compiler_Dyn.dyn -> Prims.bool ;
-  dep_scan: dep_scan_callbacks -> FStar_Compiler_Dyn.dyn -> unit }
+  to_string: FStar_Dyn.dyn -> Prims.string ;
+  eq: FStar_Dyn.dyn -> FStar_Dyn.dyn -> Prims.bool ;
+  dep_scan: dep_scan_callbacks -> FStar_Dyn.dyn -> unit }
 let (__proj__Mkto_be_desugared__item__lang_name :
   to_be_desugared -> Prims.string) =
   fun projectee ->
     match projectee with
     | { lang_name; blob; idents; to_string; eq; dep_scan;_} -> lang_name
 let (__proj__Mkto_be_desugared__item__blob :
-  to_be_desugared -> FStar_Compiler_Dyn.dyn) =
+  to_be_desugared -> FStar_Dyn.dyn) =
   fun projectee ->
     match projectee with
     | { lang_name; blob; idents; to_string; eq; dep_scan;_} -> blob
@@ -860,19 +860,17 @@ let (__proj__Mkto_be_desugared__item__idents :
     match projectee with
     | { lang_name; blob; idents; to_string; eq; dep_scan;_} -> idents
 let (__proj__Mkto_be_desugared__item__to_string :
-  to_be_desugared -> FStar_Compiler_Dyn.dyn -> Prims.string) =
+  to_be_desugared -> FStar_Dyn.dyn -> Prims.string) =
   fun projectee ->
     match projectee with
     | { lang_name; blob; idents; to_string; eq; dep_scan;_} -> to_string
 let (__proj__Mkto_be_desugared__item__eq :
-  to_be_desugared ->
-    FStar_Compiler_Dyn.dyn -> FStar_Compiler_Dyn.dyn -> Prims.bool)
-  =
+  to_be_desugared -> FStar_Dyn.dyn -> FStar_Dyn.dyn -> Prims.bool) =
   fun projectee ->
     match projectee with
     | { lang_name; blob; idents; to_string; eq; dep_scan;_} -> eq
 let (__proj__Mkto_be_desugared__item__dep_scan :
-  to_be_desugared -> dep_scan_callbacks -> FStar_Compiler_Dyn.dyn -> unit) =
+  to_be_desugared -> dep_scan_callbacks -> FStar_Dyn.dyn -> unit) =
   fun projectee ->
     match projectee with
     | { lang_name; blob; idents; to_string; eq; dep_scan;_} -> dep_scan
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Embeddings.ml
index 8d0a7c7d145..e044c7b5bef 100644
--- a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Embeddings.ml
+++ b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Embeddings.ml
@@ -266,9 +266,7 @@ let (e_env :
           FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_env;
           FStar_Syntax_Syntax.ltyp = uu___1;
           FStar_Syntax_Syntax.rng = uu___2;_}
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___1 -> FStar_Pervasives_Native.None in
   mk_emb embed_env unembed_env FStar_Reflection_V1_Constants.fstar_refl_env
 let (e_const :
@@ -1450,9 +1448,7 @@ let (e_sigelt :
           FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_sigelt;
           FStar_Syntax_Syntax.ltyp = uu___1;
           FStar_Syntax_Syntax.rng = uu___2;_}
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___1 -> FStar_Pervasives_Native.None in
   mk_emb embed_sigelt unembed_sigelt
     FStar_Reflection_V1_Constants.fstar_refl_sigelt
@@ -1548,9 +1544,7 @@ let (e_letbinding :
           FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_letbinding;
           FStar_Syntax_Syntax.ltyp = uu___1;
           FStar_Syntax_Syntax.rng = uu___2;_}
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn lb in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn lb)
     | uu___1 -> FStar_Pervasives_Native.None in
   mk_emb embed_letbinding unembed_letbinding
     FStar_Reflection_V1_Constants.fstar_refl_letbinding
@@ -2023,7 +2017,7 @@ let (e_qualifiers :
 let (unfold_lazy_bv :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let bv = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let bv = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2037,7 +2031,7 @@ let (unfold_lazy_bv :
 let (unfold_lazy_binder :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let binder = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let binder = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2051,7 +2045,7 @@ let (unfold_lazy_binder :
 let (unfold_lazy_letbinding :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let lb = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let lb = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let lbv = FStar_Reflection_V1_Builtins.inspect_lb lb in
     let uu___ =
       let uu___1 =
@@ -2087,7 +2081,7 @@ let (unfold_lazy_letbinding :
 let (unfold_lazy_fvar :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let fv = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let fv = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2102,7 +2096,7 @@ let (unfold_lazy_fvar :
 let (unfold_lazy_comp :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let comp = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let comp = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2122,7 +2116,7 @@ let (unfold_lazy_optionstate :
 let (unfold_lazy_sigelt :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let sigelt = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let sigelt = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2136,7 +2130,7 @@ let (unfold_lazy_sigelt :
 let (unfold_lazy_universe :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let u = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let u = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V1_NBEEmbeddings.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V1_NBEEmbeddings.ml
index cb80bae7698..e902e126c73 100644
--- a/ocaml/fstar-lib/generated/FStar_Reflection_V1_NBEEmbeddings.ml
+++ b/ocaml/fstar-lib/generated/FStar_Reflection_V1_NBEEmbeddings.ml
@@ -57,9 +57,8 @@ let mk_lazy :
       fun ty ->
         fun kind ->
           let li =
-            let uu___ = FStar_Compiler_Dyn.mkdyn obj in
             {
-              FStar_Syntax_Syntax.blob = uu___;
+              FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn obj);
               FStar_Syntax_Syntax.lkind = kind;
               FStar_Syntax_Syntax.ltyp = ty;
               FStar_Syntax_Syntax.rng = FStar_Compiler_Range_Type.dummyRange
@@ -85,9 +84,7 @@ let (e_bv : FStar_Syntax_Syntax.bv FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -111,9 +108,7 @@ let (e_binder :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -254,9 +249,7 @@ let (e_fv : FStar_Syntax_Syntax.fv FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -279,9 +272,7 @@ let (e_comp : FStar_Syntax_Syntax.comp FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -305,9 +296,7 @@ let (e_env : FStar_TypeChecker_Env.env FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -468,9 +457,7 @@ let (e_universe :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -680,7 +667,7 @@ let unlazy_as_t :
           when
           FStar_Class_Deq.op_Equals_Question
             FStar_Syntax_Syntax.deq_lazy_kind k k'
-          -> FStar_Compiler_Dyn.undyn v
+          -> FStar_Dyn.undyn v
       | uu___ ->
           FStar_Compiler_Effect.failwith
             "Not a Lazy of the expected kind (NBE)"
@@ -1703,9 +1690,7 @@ let (e_sigelt :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -1834,9 +1819,7 @@ let (e_letbinding :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn lb in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn lb)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Embeddings.ml
index 918c29e42e9..4bfc46ba7ff 100644
--- a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Embeddings.ml
+++ b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Embeddings.ml
@@ -2523,7 +2523,7 @@ let (e_qualifiers :
 let (unfold_lazy_bv :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let bv = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let bv = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2537,7 +2537,7 @@ let (unfold_lazy_bv :
 let (unfold_lazy_namedv :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let namedv1 = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let namedv1 = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2551,7 +2551,7 @@ let (unfold_lazy_namedv :
 let (unfold_lazy_binder :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let binder = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let binder = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2565,7 +2565,7 @@ let (unfold_lazy_binder :
 let (unfold_lazy_letbinding :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let lb = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let lb = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let lbv = FStar_Reflection_V2_Builtins.inspect_lb lb in
     let uu___ =
       let uu___1 =
@@ -2601,7 +2601,7 @@ let (unfold_lazy_letbinding :
 let (unfold_lazy_fvar :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let fv = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let fv = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2616,7 +2616,7 @@ let (unfold_lazy_fvar :
 let (unfold_lazy_comp :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let comp = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let comp = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2636,7 +2636,7 @@ let (unfold_lazy_optionstate :
 let (unfold_lazy_sigelt :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let sigelt = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let sigelt = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2650,7 +2650,7 @@ let (unfold_lazy_sigelt :
 let (unfold_lazy_universe :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let u = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let u = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let uu___ =
       let uu___1 =
         let uu___2 =
@@ -2664,7 +2664,7 @@ let (unfold_lazy_universe :
 let (unfold_lazy_doc :
   FStar_Syntax_Syntax.lazyinfo -> FStar_Syntax_Syntax.term) =
   fun i ->
-    let d = FStar_Compiler_Dyn.undyn i.FStar_Syntax_Syntax.blob in
+    let d = FStar_Dyn.undyn i.FStar_Syntax_Syntax.blob in
     let lid = FStar_Ident.lid_of_str "FStar.Stubs.Pprint.arbitrary_string" in
     let s = FStar_Pprint.render d in
     let uu___ = FStar_Syntax_Syntax.fvar lid FStar_Pervasives_Native.None in
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_NBEEmbeddings.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_NBEEmbeddings.ml
index d9c1ed8d6ae..24f09e5d227 100644
--- a/ocaml/fstar-lib/generated/FStar_Reflection_V2_NBEEmbeddings.ml
+++ b/ocaml/fstar-lib/generated/FStar_Reflection_V2_NBEEmbeddings.ml
@@ -57,9 +57,8 @@ let mk_lazy :
       fun ty ->
         fun kind ->
           let li =
-            let uu___ = FStar_Compiler_Dyn.mkdyn obj in
             {
-              FStar_Syntax_Syntax.blob = uu___;
+              FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn obj);
               FStar_Syntax_Syntax.lkind = kind;
               FStar_Syntax_Syntax.ltyp = ty;
               FStar_Syntax_Syntax.rng = FStar_Compiler_Range_Type.dummyRange
@@ -85,9 +84,7 @@ let (e_bv : FStar_Syntax_Syntax.bv FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -111,9 +108,7 @@ let (e_namedv :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -138,9 +133,7 @@ let (e_binder :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -281,9 +274,7 @@ let (e_fv : FStar_Syntax_Syntax.fv FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -306,9 +297,7 @@ let (e_comp : FStar_Syntax_Syntax.comp FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -332,9 +321,7 @@ let (e_env : FStar_TypeChecker_Env.env FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -495,9 +482,7 @@ let (e_universe :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -709,7 +694,7 @@ let unlazy_as_t :
           when
           FStar_Class_Deq.op_Equals_Question
             FStar_Syntax_Syntax.deq_lazy_kind k k'
-          -> FStar_Compiler_Dyn.undyn v
+          -> FStar_Dyn.undyn v
       | uu___ ->
           FStar_Compiler_Effect.failwith
             "Not a Lazy of the expected kind (NBE)"
@@ -726,9 +711,7 @@ let (e_ident : FStar_Ident.ident FStar_TypeChecker_NBETerm.embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -2047,9 +2030,7 @@ let (e_sigelt :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
@@ -2171,9 +2152,7 @@ let (e_letbinding :
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn lb in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn lb)
     | uu___ ->
         ((let uu___2 =
             let uu___3 =
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml
index 32256ce5c33..4bdaa25aa82 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml
@@ -140,7 +140,7 @@ let lazy_unembed :
                     else ());
                    res)
                 else
-                  (let a1 = FStar_Compiler_Dyn.undyn b in
+                  (let a1 = FStar_Dyn.undyn b in
                    (let uu___5 =
                       FStar_Compiler_Effect.op_Bang
                         FStar_Options.debug_embedding in
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml
index 1d55cebd6d0..d1533f4bcda 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml
@@ -290,9 +290,7 @@ let e_lazy :
             when
             FStar_Class_Deq.op_Equals_Question
               FStar_Syntax_Syntax.deq_lazy_kind lkind k
-            ->
-            let uu___3 = FStar_Compiler_Dyn.undyn b in
-            FStar_Pervasives_Native.Some uu___3
+            -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
         | FStar_Syntax_Syntax.Tm_lazy
             { FStar_Syntax_Syntax.blob = b;
               FStar_Syntax_Syntax.lkind = lkind;
@@ -407,7 +405,7 @@ let lazy_unembed :
                     else ());
                    res)
                 else
-                  (let a1 = FStar_Compiler_Dyn.undyn b in
+                  (let a1 = FStar_Dyn.undyn b in
                    (let uu___5 =
                       FStar_Compiler_Effect.op_Bang
                         FStar_Options.debug_embedding in
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
index 08a9131e5b2..cc8b5631f7d 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
@@ -392,7 +392,7 @@ and residual_comp =
   residual_flags: cflag Prims.list }
 and lazyinfo =
   {
-  blob: FStar_Compiler_Dyn.dyn ;
+  blob: FStar_Dyn.dyn ;
   lkind: lazy_kind ;
   ltyp: term' syntax ;
   rng: FStar_Compiler_Range_Type.range }
@@ -1011,7 +1011,7 @@ let (__proj__Mkresidual_comp__item__residual_flags :
   fun projectee ->
     match projectee with
     | { residual_effect; residual_typ; residual_flags;_} -> residual_flags
-let (__proj__Mklazyinfo__item__blob : lazyinfo -> FStar_Compiler_Dyn.dyn) =
+let (__proj__Mklazyinfo__item__blob : lazyinfo -> FStar_Dyn.dyn) =
   fun projectee -> match projectee with | { blob; lkind; ltyp; rng;_} -> blob
 let (__proj__Mklazyinfo__item__lkind : lazyinfo -> lazy_kind) =
   fun projectee ->
@@ -1707,7 +1707,7 @@ type sig_metadata =
   sigmeta_admit: Prims.bool ;
   sigmeta_spliced: Prims.bool ;
   sigmeta_already_checked: Prims.bool ;
-  sigmeta_extension_data: (Prims.string * FStar_Compiler_Dyn.dyn) Prims.list }
+  sigmeta_extension_data: (Prims.string * FStar_Dyn.dyn) Prims.list }
 let (__proj__Mksig_metadata__item__sigmeta_active :
   sig_metadata -> Prims.bool) =
   fun projectee ->
@@ -1741,7 +1741,7 @@ let (__proj__Mksig_metadata__item__sigmeta_already_checked :
         sigmeta_already_checked; sigmeta_extension_data;_} ->
         sigmeta_already_checked
 let (__proj__Mksig_metadata__item__sigmeta_extension_data :
-  sig_metadata -> (Prims.string * FStar_Compiler_Dyn.dyn) Prims.list) =
+  sig_metadata -> (Prims.string * FStar_Dyn.dyn) Prims.list) =
   fun projectee ->
     match projectee with
     | { sigmeta_active; sigmeta_fact_db_ids; sigmeta_admit; sigmeta_spliced;
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
index 7a45dc0d374..a33dd2345a2 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
@@ -888,7 +888,7 @@ let unlazy_as_t :
             FStar_Class_Deq.op_Equals_Question
               FStar_Syntax_Syntax.deq_lazy_kind k k' in
           if uu___3
-          then FStar_Compiler_Dyn.undyn v
+          then FStar_Dyn.undyn v
           else
             (let uu___5 =
                let uu___6 =
@@ -920,9 +920,8 @@ let mk_lazy :
             | FStar_Pervasives_Native.None ->
                 FStar_Compiler_Range_Type.dummyRange in
           let i =
-            let uu___ = FStar_Compiler_Dyn.mkdyn t in
             {
-              FStar_Syntax_Syntax.blob = uu___;
+              FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn t);
               FStar_Syntax_Syntax.lkind = k;
               FStar_Syntax_Syntax.ltyp = typ;
               FStar_Syntax_Syntax.rng = rng
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml
index d451bcb7e59..53ce5affc80 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml
@@ -214,9 +214,8 @@ let (e_proofstate_nbe :
   FStar_Tactics_Types.proofstate FStar_TypeChecker_NBETerm.embedding) =
   let embed_proofstate _cb ps =
     let li =
-      let uu___ = FStar_Compiler_Dyn.mkdyn ps in
       {
-        FStar_Syntax_Syntax.blob = uu___;
+        FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn ps);
         FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_proofstate;
         FStar_Syntax_Syntax.ltyp = (fstar_tactics_proofstate.t);
         FStar_Syntax_Syntax.rng = FStar_Compiler_Range_Type.dummyRange
@@ -241,9 +240,7 @@ let (e_proofstate_nbe :
            FStar_Syntax_Syntax.ltyp = uu___1;
            FStar_Syntax_Syntax.rng = uu___2;_},
          uu___3)
-        ->
-        let uu___4 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___4
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___1 ->
         ((let uu___3 =
             FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in
@@ -271,9 +268,8 @@ let (e_goal_nbe :
   FStar_Tactics_Types.goal FStar_TypeChecker_NBETerm.embedding) =
   let embed_goal _cb ps =
     let li =
-      let uu___ = FStar_Compiler_Dyn.mkdyn ps in
       {
-        FStar_Syntax_Syntax.blob = uu___;
+        FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn ps);
         FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_goal;
         FStar_Syntax_Syntax.ltyp = (fstar_tactics_goal.t);
         FStar_Syntax_Syntax.rng = FStar_Compiler_Range_Type.dummyRange
@@ -297,9 +293,7 @@ let (e_goal_nbe :
            FStar_Syntax_Syntax.ltyp = uu___1;
            FStar_Syntax_Syntax.rng = uu___2;_},
          uu___3)
-        ->
-        let uu___4 = FStar_Compiler_Dyn.undyn b in
-        FStar_Pervasives_Native.Some uu___4
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
     | uu___1 ->
         ((let uu___3 =
             FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in
@@ -909,9 +903,7 @@ let e_tref :
             FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_tref;
             FStar_Syntax_Syntax.ltyp = uu___3;
             FStar_Syntax_Syntax.rng = uu___4;_}
-          ->
-          let uu___5 = FStar_Compiler_Dyn.undyn blob in
-          FStar_Pervasives_Native.Some uu___5
+          -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn blob)
       | uu___3 -> FStar_Pervasives_Native.None in
     FStar_Syntax_Embeddings_Base.mk_emb_full em un (fun uu___1 -> t_tref)
       (fun i -> "tref")
@@ -927,9 +919,8 @@ let e_tref_nbe :
   fun uu___ ->
     let embed_tref _cb r =
       let li =
-        let uu___1 = FStar_Compiler_Dyn.mkdyn r in
         {
-          FStar_Syntax_Syntax.blob = uu___1;
+          FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn r);
           FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_tref;
           FStar_Syntax_Syntax.ltyp = t_tref;
           FStar_Syntax_Syntax.rng = FStar_Compiler_Range_Type.dummyRange
@@ -953,9 +944,7 @@ let e_tref_nbe :
              FStar_Syntax_Syntax.ltyp = uu___2;
              FStar_Syntax_Syntax.rng = uu___3;_},
            uu___4)
-          ->
-          let uu___5 = FStar_Compiler_Dyn.undyn b in
-          FStar_Pervasives_Native.Some uu___5
+          -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn b)
       | uu___2 ->
           ((let uu___4 =
               FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml
index 94ef5fa3595..e29dd541d69 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml
@@ -2012,39 +2012,6 @@ let (splice :
                                           (fun uu___9 ->
                                              match uu___9 with
                                              | (checked, se, blob_opt) ->
-                                                 let uu___10 =
-                                                   let uu___11 =
-                                                     se.FStar_Syntax_Syntax.sigmeta in
-                                                   let uu___12 =
-                                                     match blob_opt with
-                                                     | FStar_Pervasives_Native.Some
-                                                         (s, blob) ->
-                                                         let uu___13 =
-                                                           let uu___14 =
-                                                             FStar_Compiler_Dyn.mkdyn
-                                                               blob in
-                                                           (s, uu___14) in
-                                                         [uu___13]
-                                                     | FStar_Pervasives_Native.None
-                                                         -> [] in
-                                                   {
-                                                     FStar_Syntax_Syntax.sigmeta_active
-                                                       =
-                                                       (uu___11.FStar_Syntax_Syntax.sigmeta_active);
-                                                     FStar_Syntax_Syntax.sigmeta_fact_db_ids
-                                                       =
-                                                       (uu___11.FStar_Syntax_Syntax.sigmeta_fact_db_ids);
-                                                     FStar_Syntax_Syntax.sigmeta_admit
-                                                       =
-                                                       (uu___11.FStar_Syntax_Syntax.sigmeta_admit);
-                                                     FStar_Syntax_Syntax.sigmeta_spliced
-                                                       =
-                                                       (uu___11.FStar_Syntax_Syntax.sigmeta_spliced);
-                                                     FStar_Syntax_Syntax.sigmeta_already_checked
-                                                       = checked;
-                                                     FStar_Syntax_Syntax.sigmeta_extension_data
-                                                       = uu___12
-                                                   } in
                                                  {
                                                    FStar_Syntax_Syntax.sigel
                                                      =
@@ -2056,7 +2023,36 @@ let (splice :
                                                      =
                                                      (se.FStar_Syntax_Syntax.sigquals);
                                                    FStar_Syntax_Syntax.sigmeta
-                                                     = uu___10;
+                                                     =
+                                                     (let uu___10 =
+                                                        se.FStar_Syntax_Syntax.sigmeta in
+                                                      {
+                                                        FStar_Syntax_Syntax.sigmeta_active
+                                                          =
+                                                          (uu___10.FStar_Syntax_Syntax.sigmeta_active);
+                                                        FStar_Syntax_Syntax.sigmeta_fact_db_ids
+                                                          =
+                                                          (uu___10.FStar_Syntax_Syntax.sigmeta_fact_db_ids);
+                                                        FStar_Syntax_Syntax.sigmeta_admit
+                                                          =
+                                                          (uu___10.FStar_Syntax_Syntax.sigmeta_admit);
+                                                        FStar_Syntax_Syntax.sigmeta_spliced
+                                                          =
+                                                          (uu___10.FStar_Syntax_Syntax.sigmeta_spliced);
+                                                        FStar_Syntax_Syntax.sigmeta_already_checked
+                                                          = checked;
+                                                        FStar_Syntax_Syntax.sigmeta_extension_data
+                                                          =
+                                                          ((match blob_opt
+                                                            with
+                                                            | FStar_Pervasives_Native.Some
+                                                                (s, blob) ->
+                                                                [(s,
+                                                                   (FStar_Dyn.mkdyn
+                                                                    blob))]
+                                                            | FStar_Pervasives_Native.None
+                                                                -> []))
+                                                      });
                                                    FStar_Syntax_Syntax.sigattrs
                                                      =
                                                      (se.FStar_Syntax_Syntax.sigattrs);
diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
index f0e5b67af2c..a16843f80af 100644
--- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
@@ -1,7 +1,7 @@
 open Prims
 type extension_tosyntax_decl_t =
   FStar_Syntax_DsEnv.env ->
-    FStar_Compiler_Dyn.dyn ->
+    FStar_Dyn.dyn ->
       FStar_Ident.lident Prims.list ->
         FStar_Compiler_Range_Type.range ->
           FStar_Syntax_Syntax.sigelt' Prims.list
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml
index 5e19501b315..3eec03cdace 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml
@@ -85,8 +85,8 @@ and t' =
   | Reflect of t 
   | Quote of (FStar_Syntax_Syntax.term * FStar_Syntax_Syntax.quoteinfo) 
   | Lazy of ((FStar_Syntax_Syntax.lazyinfo,
-  (FStar_Compiler_Dyn.dyn * FStar_Syntax_Syntax.emb_typ))
-  FStar_Pervasives.either * t FStar_Thunk.t) 
+  (FStar_Dyn.dyn * FStar_Syntax_Syntax.emb_typ)) FStar_Pervasives.either * t
+  FStar_Thunk.t) 
   | Meta of (t * FStar_Syntax_Syntax.metadata FStar_Thunk.t) 
   | TopLevelLet of (FStar_Syntax_Syntax.letbinding * Prims.int * (t *
   FStar_Syntax_Syntax.aqual) Prims.list) 
@@ -258,8 +258,8 @@ let (uu___is_Lazy : t' -> Prims.bool) =
 let (__proj__Lazy__item___0 :
   t' ->
     ((FStar_Syntax_Syntax.lazyinfo,
-      (FStar_Compiler_Dyn.dyn * FStar_Syntax_Syntax.emb_typ))
-      FStar_Pervasives.either * t FStar_Thunk.t))
+      (FStar_Dyn.dyn * FStar_Syntax_Syntax.emb_typ)) FStar_Pervasives.either
+      * t FStar_Thunk.t))
   = fun projectee -> match projectee with | Lazy _0 -> _0
 let (uu___is_Meta : t' -> Prims.bool) =
   fun projectee -> match projectee with | Meta _0 -> true | uu___ -> false
@@ -913,9 +913,7 @@ let lazy_embed :
          then f ()
          else
            (let thunk = FStar_Thunk.mk f in
-            let li =
-              let uu___3 = FStar_Compiler_Dyn.mkdyn x in
-              let uu___4 = et () in (uu___3, uu___4) in
+            let li = let uu___3 = et () in ((FStar_Dyn.mkdyn x), uu___3) in
             mk_t (Lazy ((FStar_Pervasives.Inr li), thunk))))
 let lazy_unembed :
   'a .
@@ -953,7 +951,7 @@ let lazy_unembed :
                 else ());
                res)
             else
-              (let a1 = FStar_Compiler_Dyn.undyn b in
+              (let a1 = FStar_Dyn.undyn b in
                (let uu___3 =
                   FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in
                 if uu___3
@@ -990,8 +988,8 @@ let lazy_unembed_lazy_kind :
       | Lazy (FStar_Pervasives.Inl li, uu___) ->
           if li.FStar_Syntax_Syntax.lkind = k
           then
-            let uu___1 = FStar_Compiler_Dyn.undyn li.FStar_Syntax_Syntax.blob in
-            FStar_Pervasives_Native.Some uu___1
+            FStar_Pervasives_Native.Some
+              (FStar_Dyn.undyn li.FStar_Syntax_Syntax.blob)
           else FStar_Pervasives_Native.None
       | uu___ -> FStar_Pervasives_Native.None
 type abstract_nbe_term =
@@ -1356,9 +1354,8 @@ let (e_issue : FStar_Errors.issue embedding) =
   let t_issue =
     FStar_Syntax_Embeddings_Base.type_of FStar_Syntax_Embeddings.e_issue in
   let li blob rng =
-    let uu___ = FStar_Compiler_Dyn.mkdyn blob in
     {
-      FStar_Syntax_Syntax.blob = uu___;
+      FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn blob);
       FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_issue;
       FStar_Syntax_Syntax.ltyp = t_issue;
       FStar_Syntax_Syntax.rng = rng
@@ -1366,13 +1363,11 @@ let (e_issue : FStar_Errors.issue embedding) =
   let em1 cb iss =
     let uu___ =
       let uu___1 =
-        let uu___2 = li iss FStar_Compiler_Range_Type.dummyRange in
-        FStar_Pervasives.Inl uu___2 in
-      let uu___2 =
         FStar_Thunk.mk
-          (fun uu___3 ->
+          (fun uu___2 ->
              FStar_Compiler_Effect.failwith "Cannot unembed issue") in
-      (uu___1, uu___2) in
+      ((FStar_Pervasives.Inl (li iss FStar_Compiler_Range_Type.dummyRange)),
+        uu___1) in
     Lazy uu___ in
   let un1 cb t1 =
     match t1 with
@@ -1383,9 +1378,7 @@ let (e_issue : FStar_Errors.issue embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn blob in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn blob)
     | uu___ -> FStar_Pervasives_Native.None in
   mk_emb' em1 un1
     (fun uu___ -> lid_as_typ FStar_Parser_Const.issue_lid [] [])
@@ -1394,9 +1387,8 @@ let (e_document : FStar_Pprint.document embedding) =
   let t_document =
     FStar_Syntax_Embeddings_Base.type_of FStar_Syntax_Embeddings.e_document in
   let li blob rng =
-    let uu___ = FStar_Compiler_Dyn.mkdyn blob in
     {
-      FStar_Syntax_Syntax.blob = uu___;
+      FStar_Syntax_Syntax.blob = (FStar_Dyn.mkdyn blob);
       FStar_Syntax_Syntax.lkind = FStar_Syntax_Syntax.Lazy_doc;
       FStar_Syntax_Syntax.ltyp = t_document;
       FStar_Syntax_Syntax.rng = rng
@@ -1404,13 +1396,11 @@ let (e_document : FStar_Pprint.document embedding) =
   let em1 cb doc =
     let uu___ =
       let uu___1 =
-        let uu___2 = li doc FStar_Compiler_Range_Type.dummyRange in
-        FStar_Pervasives.Inl uu___2 in
-      let uu___2 =
         FStar_Thunk.mk
-          (fun uu___3 ->
+          (fun uu___2 ->
              FStar_Compiler_Effect.failwith "Cannot unembed document") in
-      (uu___1, uu___2) in
+      ((FStar_Pervasives.Inl (li doc FStar_Compiler_Range_Type.dummyRange)),
+        uu___1) in
     Lazy uu___ in
   let un1 cb t1 =
     match t1 with
@@ -1421,9 +1411,7 @@ let (e_document : FStar_Pprint.document embedding) =
            FStar_Syntax_Syntax.ltyp = uu___;
            FStar_Syntax_Syntax.rng = uu___1;_},
          uu___2)
-        ->
-        let uu___3 = FStar_Compiler_Dyn.undyn blob in
-        FStar_Pervasives_Native.Some uu___3
+        -> FStar_Pervasives_Native.Some (FStar_Dyn.undyn blob)
     | uu___ -> FStar_Pervasives_Native.None in
   mk_emb' em1 un1
     (fun uu___ -> lid_as_typ FStar_Parser_Const.document_lid [] [])
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Array.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Array.ml
index dee26997e27..d7a4a002958 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Array.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Array.ml
@@ -205,12 +205,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) =
                   match uu___ with
                   | (l, lst) ->
                       let blob = FStar_ImmutableArray_Base.of_list lst in
-                      let uu___1 =
-                        let uu___2 =
-                          let uu___3 = FStar_Compiler_Dyn.mkdyn blob in
-                          (l, uu___3) in
-                        (universes, elt_t, uu___2) in
-                      FStar_Pervasives_Native.Some uu___1)),
+                      FStar_Pervasives_Native.Some
+                        (universes, elt_t, (l, (FStar_Dyn.mkdyn blob))))),
       (FStar_TypeChecker_NBETerm.mixed_binary_op
          (fun uu___ ->
             match uu___ with
@@ -265,12 +261,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) =
                 match uu___ with
                 | (l, lst) ->
                     let blob = FStar_ImmutableArray_Base.of_list lst in
-                    let uu___1 =
-                      let uu___2 =
-                        let uu___3 = FStar_Compiler_Dyn.mkdyn blob in
-                        (l, uu___3) in
-                      (universes, elt_t, uu___2) in
-                    FStar_Pervasives_Native.Some uu___1))) in
+                    FStar_Pervasives_Native.Some
+                      (universes, elt_t, (l, (FStar_Dyn.mkdyn blob)))))) in
   let arg1_as_elt_t x =
     FStar_Pervasives_Native.Some (FStar_Pervasives_Native.fst x) in
   let arg2_as_blob x =
@@ -306,9 +298,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) =
       FStar_TypeChecker_Primops_Base.embed_simple
         FStar_Syntax_Embeddings.e_int r i in
     let run_op blob =
-      let uu___ =
-        let uu___1 = FStar_Compiler_Dyn.undyn blob in
-        FStar_Compiler_Util.array_length uu___1 in
+      let uu___ = FStar_Compiler_Util.array_length (FStar_Dyn.undyn blob) in
       FStar_Pervasives_Native.Some uu___ in
     (FStar_Parser_Const.immutable_array_length_lid, (Prims.of_int (2)),
       Prims.int_one,
@@ -334,8 +324,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) =
                 fun blob ->
                   fun i ->
                     let uu___ =
-                      let uu___1 = FStar_Compiler_Dyn.undyn blob in
-                      FStar_Compiler_Util.array_index uu___1 i in
+                      FStar_Compiler_Util.array_index (FStar_Dyn.undyn blob)
+                        i in
                     FStar_Pervasives_Native.Some uu___)),
       (FStar_TypeChecker_NBETerm.mixed_ternary_op
          (fun uu___ ->
@@ -347,8 +337,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) =
               fun blob ->
                 fun i ->
                   let uu___ =
-                    let uu___1 = FStar_Compiler_Dyn.undyn blob in
-                    FStar_Compiler_Util.array_index uu___1 i in
+                    FStar_Compiler_Util.array_index (FStar_Dyn.undyn blob) i in
                   FStar_Pervasives_Native.Some uu___))) in
   FStar_Compiler_List.map (as_primitive_step true)
     [of_list_op; length_op; index_op]
\ No newline at end of file
diff --git a/src/basic/FStar.Compiler.Dyn.fsti b/src/basic/FStar.Compiler.Dyn.fsti
deleted file mode 100644
index c2a822ced5e..00000000000
--- a/src/basic/FStar.Compiler.Dyn.fsti
+++ /dev/null
@@ -1,16 +0,0 @@
-module FStar.Compiler.Dyn
-open FStar.Compiler.Effect
-
-///  Dynamic casts, realized by OCaml's [Obj]
-///
-///  NOTE: THIS PROVIDES CASTS BETWEEN ARBITRARY TYPES
-///  BUT ONLY IN [False] CONTEXTS. USE WISELY.
-assume new
-type dyn
-
-(** Promoting a value of type ['a] to [dyn] *)
-val mkdyn: 'a -> ML dyn
-
-(** This coerces a value of type [dyn] to any type ['a],
-    but only with [False] precondition *)
-val undyn (d: dyn{false}) : ML 'a
diff --git a/src/basic/FStar.Compiler.Effect.fst b/src/basic/FStar.Compiler.Effect.fst
index 60070492648..3fdae4a5759 100644
--- a/src/basic/FStar.Compiler.Effect.fst
+++ b/src/basic/FStar.Compiler.Effect.fst
@@ -29,6 +29,7 @@ let lift_pure_all (a:Type) (p:pure_wp a)
 
 sub_effect PURE ~> ALL { lift_wp = lift_pure_all }
 
+sub_effect DIV ~> ALL { lift_wp = lift_pure_all }
 
 effect All (a:Type) (pre:all_pre) (post:(h:unit -> Tot (all_post' a (pre h)))) =
   ALL a
diff --git a/src/extraction/FStar.Extraction.ML.Modul.fsti b/src/extraction/FStar.Extraction.ML.Modul.fsti
index e0e4c289d6c..9952a983920 100644
--- a/src/extraction/FStar.Extraction.ML.Modul.fsti
+++ b/src/extraction/FStar.Extraction.ML.Modul.fsti
@@ -25,9 +25,9 @@ module S = FStar.Syntax.Syntax
 val iface : Type0
 
 type extension_sigelt_extractor =
-  uenv -> sigelt -> FStar.Compiler.Dyn.dyn -> either mlmodule string
+  uenv -> sigelt -> FStar.Dyn.dyn -> either mlmodule string
 type extension_sigelt_iface_extractor =
-  uenv -> sigelt -> FStar.Compiler.Dyn.dyn -> either (uenv & iface) string
+  uenv -> sigelt -> FStar.Dyn.dyn -> either (uenv & iface) string
 
 type extension_extractor = {
    extract_sigelt : extension_sigelt_extractor;
diff --git a/src/parser/FStar.Parser.AST.fsti b/src/parser/FStar.Parser.AST.fsti
index 570a3622262..2d0f6e2f40f 100644
--- a/src/parser/FStar.Parser.AST.fsti
+++ b/src/parser/FStar.Parser.AST.fsti
@@ -230,11 +230,11 @@ type dep_scan_callbacks = {
 
 type to_be_desugared = {
   lang_name: string;
-  blob: FStar.Compiler.Dyn.dyn;
+  blob: FStar.Dyn.dyn;
   idents: list ident;
-  to_string: FStar.Compiler.Dyn.dyn -> string;
-  eq: FStar.Compiler.Dyn.dyn -> FStar.Compiler.Dyn.dyn -> bool;
-  dep_scan: dep_scan_callbacks -> FStar.Compiler.Dyn.dyn -> unit
+  to_string: FStar.Dyn.dyn -> string;
+  eq: FStar.Dyn.dyn -> FStar.Dyn.dyn -> bool;
+  dep_scan: dep_scan_callbacks -> FStar.Dyn.dyn -> unit
 }
 
 type decl' =
@@ -353,4 +353,4 @@ val ident_of_binder : range -> binder -> ident
 val idents_of_binders : list binder -> range -> list ident
 
 instance val showable_decl : showable decl
-instance val showable_term : showable term
\ No newline at end of file
+instance val showable_term : showable term
diff --git a/src/reflection/FStar.Reflection.V1.Builtins.fst b/src/reflection/FStar.Reflection.V1.Builtins.fst
index 4652661bf5b..ca28e043b36 100644
--- a/src/reflection/FStar.Reflection.V1.Builtins.fst
+++ b/src/reflection/FStar.Reflection.V1.Builtins.fst
@@ -45,7 +45,7 @@ module EMB   = FStar.Syntax.Embeddings
 module N     = FStar.TypeChecker.Normalize
 open FStar.VConfig
 
-open FStar.Compiler.Dyn
+open FStar.Dyn
 
 (* This file provides implementation for reflection primitives in F*.
  *
diff --git a/src/reflection/FStar.Reflection.V1.Embeddings.fst b/src/reflection/FStar.Reflection.V1.Embeddings.fst
index 7881a1b64f4..ed658ac6c70 100644
--- a/src/reflection/FStar.Reflection.V1.Embeddings.fst
+++ b/src/reflection/FStar.Reflection.V1.Embeddings.fst
@@ -41,7 +41,7 @@ module Z       = FStar.BigInt
 
 module EmbV2 = FStar.Reflection.V2.Embeddings
 
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.Reflection.V1.Builtins //needed for inspect_fv, but that feels wrong
 open FStar.Reflection.V1.Constants
 
diff --git a/src/reflection/FStar.Reflection.V1.NBEEmbeddings.fst b/src/reflection/FStar.Reflection.V1.NBEEmbeddings.fst
index 37441fa4b34..37029c55f8f 100644
--- a/src/reflection/FStar.Reflection.V1.NBEEmbeddings.fst
+++ b/src/reflection/FStar.Reflection.V1.NBEEmbeddings.fst
@@ -38,7 +38,7 @@ module SS      = FStar.Syntax.Subst
 module Thunk   = FStar.Thunk
 module U       = FStar.Syntax.Util
 
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.Reflection.V1.Constants
 
 (*
@@ -66,7 +66,7 @@ let mk_emb' x y fv = mk_emb x y (fun () -> mkFV fv [] []) (fun () -> fv_as_emb_t
 
 let mk_lazy cb obj ty kind =
     let li = {
-          blob = FStar.Compiler.Dyn.mkdyn obj
+          blob = FStar.Dyn.mkdyn obj
         ; lkind = kind
         ; ltyp = ty
         ; rng = Range.dummyRange
@@ -82,7 +82,7 @@ let e_bv =
     let unembed_bv cb (t:t) : option bv =
         match t.nbe_t with
         | Lazy (Inl {blob=b; lkind=Lazy_bv}, _) ->
-            Some <| FStar.Compiler.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
             Err.log_issue Range.dummyRange (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded bv: %s" (t_to_string t)));
             None
@@ -324,7 +324,7 @@ let unlazy_as_t k t =
     let open FStar.Class.Deq in
     match t.nbe_t with
     | Lazy (Inl {lkind=k'; blob=v}, _) when k =? k' ->
-      FStar.Compiler.Dyn.undyn v
+      FStar.Dyn.undyn v
     | _ ->
       failwith "Not a Lazy of the expected kind (NBE)"
 
diff --git a/src/reflection/FStar.Reflection.V2.Builtins.fst b/src/reflection/FStar.Reflection.V2.Builtins.fst
index 484a5925f37..484f0f5213b 100644
--- a/src/reflection/FStar.Reflection.V2.Builtins.fst
+++ b/src/reflection/FStar.Reflection.V2.Builtins.fst
@@ -46,7 +46,7 @@ module EMB   = FStar.Syntax.Embeddings
 module N     = FStar.TypeChecker.Normalize
 open FStar.VConfig
 
-open FStar.Compiler.Dyn
+open FStar.Dyn
 
 (* This file provides implementation for reflection primitives in F*.
  *
diff --git a/src/reflection/FStar.Reflection.V2.Embeddings.fst b/src/reflection/FStar.Reflection.V2.Embeddings.fst
index 9f83f002b4f..79769cb9a23 100644
--- a/src/reflection/FStar.Reflection.V2.Embeddings.fst
+++ b/src/reflection/FStar.Reflection.V2.Embeddings.fst
@@ -40,7 +40,7 @@ module U       = FStar.Syntax.Util
 module Z       = FStar.BigInt
 
 open FStar.Reflection.V2.Builtins //needed for inspect_fv, but that feels wrong
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.Syntax.Embeddings.AppEmb
 open FStar.Class.Monad
 
diff --git a/src/reflection/FStar.Reflection.V2.NBEEmbeddings.fst b/src/reflection/FStar.Reflection.V2.NBEEmbeddings.fst
index 918cf34ac0f..3349ce0098c 100644
--- a/src/reflection/FStar.Reflection.V2.NBEEmbeddings.fst
+++ b/src/reflection/FStar.Reflection.V2.NBEEmbeddings.fst
@@ -22,7 +22,7 @@ open FStar.Syntax.Syntax
 open FStar.TypeChecker.NBETerm
 open FStar.Order
 open FStar.Errors
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.Reflection.V2.Constants
 
 module BU      = FStar.Compiler.Util
@@ -63,7 +63,7 @@ let mk_emb' x y fv = mk_emb x y (fun () -> mkFV fv [] []) (fun () -> fv_as_emb_t
 
 let mk_lazy cb obj ty kind =
     let li = {
-          blob = FStar.Compiler.Dyn.mkdyn obj
+          blob = FStar.Dyn.mkdyn obj
         ; lkind = kind
         ; ltyp = ty
         ; rng = Range.dummyRange
@@ -79,7 +79,7 @@ let e_bv =
     let unembed_bv cb (t:t) : option bv =
         match t.nbe_t with
         | Lazy (Inl {blob=b; lkind=Lazy_bv}, _) ->
-            Some <| FStar.Compiler.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
             Err.log_issue Range.dummyRange (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded bv: %s" (t_to_string t)));
             None
@@ -93,7 +93,7 @@ let e_namedv =
     let unembed_namedv cb (t:t) : option namedv =
         match t.nbe_t with
         | Lazy (Inl {blob=b; lkind=Lazy_namedv}, _) ->
-            Some <| FStar.Compiler.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
             Err.log_issue Range.dummyRange (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded namedv: %s" (t_to_string t)));
             None
@@ -335,7 +335,7 @@ let unlazy_as_t k t =
     match t.nbe_t with
     | Lazy (Inl {lkind=k'; blob=v}, _)
         when k =? k' ->
-      FStar.Compiler.Dyn.undyn v
+      FStar.Dyn.undyn v
     | _ ->
       failwith "Not a Lazy of the expected kind (NBE)"
 
diff --git a/src/syntax/FStar.Syntax.Syntax.fst b/src/syntax/FStar.Syntax.Syntax.fst
index 3046c83fbf4..930e6be5cea 100644
--- a/src/syntax/FStar.Syntax.Syntax.fst
+++ b/src/syntax/FStar.Syntax.Syntax.fst
@@ -24,7 +24,7 @@ open FStar.Compiler.Util
 open FStar.Compiler.Range
 open FStar.Ident
 open FStar.Const
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.VConfig
 
 open FStar.Class.Ord
diff --git a/src/syntax/FStar.Syntax.Syntax.fsti b/src/syntax/FStar.Syntax.Syntax.fsti
index efa685e6128..a31295cdd35 100644
--- a/src/syntax/FStar.Syntax.Syntax.fsti
+++ b/src/syntax/FStar.Syntax.Syntax.fsti
@@ -22,7 +22,7 @@ open FStar.Compiler
 open FStar.Compiler.Util
 open FStar.Compiler.Range
 open FStar.Ident
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.Const
 module O = FStar.Options
 open FStar.VConfig
diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst
index 4b633818051..fc87867e22e 100644
--- a/src/syntax/FStar.Syntax.Util.fst
+++ b/src/syntax/FStar.Syntax.Util.fst
@@ -27,7 +27,7 @@ open FStar.Compiler.Range
 open FStar.Syntax
 open FStar.Syntax.Syntax
 open FStar.Const
-open FStar.Compiler.Dyn
+open FStar.Dyn
 module U = FStar.Compiler.Util
 module List = FStar.Compiler.List
 module PC = FStar.Parser.Const
@@ -480,7 +480,7 @@ let unlazy_as_t k t =
     match (compress t).n with
     | Tm_lazy ({lkind=k'; blob=v}) ->
       if k =? k'
-      then FStar.Compiler.Dyn.undyn v
+      then Dyn.undyn v
       else failwith (U.format2 "Expected Tm_lazy of kind %s, got %s"
                        (show k) (show k'))
     | _ ->
diff --git a/src/tactics/FStar.Tactics.Embedding.fst b/src/tactics/FStar.Tactics.Embedding.fst
index 6cb6c514c31..f1cdaa7bd0e 100644
--- a/src/tactics/FStar.Tactics.Embedding.fst
+++ b/src/tactics/FStar.Tactics.Embedding.fst
@@ -159,7 +159,7 @@ let fv_as_emb_typ fv = S.ET_app (show fv.fv_name.v, [])
 let e_proofstate_nbe =
     let embed_proofstate _cb (ps:proofstate) : NBETerm.t =
         let li = { lkind = Lazy_proofstate
-                 ; blob = FStar.Compiler.Dyn.mkdyn ps
+                 ; blob = FStar.Dyn.mkdyn ps
                  ; ltyp = fstar_tactics_proofstate.t
                  ; rng = Range.dummyRange }
         in
@@ -169,7 +169,7 @@ let e_proofstate_nbe =
     let unembed_proofstate _cb (t:NBETerm.t) : option proofstate =
         match NBETerm.nbe_t_of_t t with
         | NBETerm.Lazy (Inl {blob=b; lkind = Lazy_proofstate}, _) ->
-            Some <| FStar.Compiler.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
           if !Options.debug_embedding then
             Err.log_issue Range.dummyRange
@@ -187,7 +187,7 @@ let e_proofstate_nbe =
 let e_goal_nbe =
     let embed_goal _cb (ps:goal) : NBETerm.t =
         let li = { lkind = Lazy_goal
-                 ; blob = FStar.Compiler.Dyn.mkdyn ps
+                 ; blob = FStar.Dyn.mkdyn ps
                  ; ltyp = fstar_tactics_goal.t
                  ; rng = Range.dummyRange }
         in
@@ -197,7 +197,7 @@ let e_goal_nbe =
     let unembed_goal _cb (t:NBETerm.t) : option goal =
         match NBETerm.nbe_t_of_t t with
         | NBETerm.Lazy (Inl {blob=b; lkind = Lazy_goal}, _) ->
-            Some <| FStar.Compiler.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
             if !Options.debug_embedding then
               Err.log_issue Range.dummyRange (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded NBE goal: %s" (NBETerm.t_to_string t)));
@@ -546,7 +546,7 @@ let e_tref #a =
 let e_tref_nbe #a =
   let embed_tref _cb (r:tref a) : NBETerm.t =
     let li = { lkind = Lazy_tref
-             ; blob = FStar.Compiler.Dyn.mkdyn r
+             ; blob = FStar.Dyn.mkdyn r
              ; ltyp = t_tref
              ; rng = Range.dummyRange }
     in
@@ -556,7 +556,7 @@ let e_tref_nbe #a =
   let unembed_tref _cb (t:NBETerm.t) : option (tref a) =
     match NBETerm.nbe_t_of_t t with
     | NBETerm.Lazy (Inl {blob=b; lkind = Lazy_tref}, _) ->
-      Some <| FStar.Compiler.Dyn.undyn b
+      Some <| FStar.Dyn.undyn b
     | _ ->
       if !Options.debug_embedding then
         Err.log_issue Range.dummyRange
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti b/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti
index 682b72eeef4..51f66d3c421 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti
@@ -30,7 +30,7 @@ open FStar.Ident
 module S = FStar.Syntax.Syntax
 module U = FStar.Syntax.Util
 
-type extension_tosyntax_decl_t = env -> FStar.Compiler.Dyn.dyn -> lids:list lident -> Range.range -> list sigelt'
+type extension_tosyntax_decl_t = env -> FStar.Dyn.dyn -> lids:list lident -> Range.range -> list sigelt'
 val register_extension_tosyntax (lang_name:string) (cb:extension_tosyntax_decl_t) : unit
 
 val as_interface:            AST.modul -> AST.modul
diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fst b/src/typechecker/FStar.TypeChecker.NBETerm.fst
index 3177d2a46d2..4cb1cdb54ec 100644
--- a/src/typechecker/FStar.TypeChecker.NBETerm.fst
+++ b/src/typechecker/FStar.TypeChecker.NBETerm.fst
@@ -277,7 +277,7 @@ let lazy_embed (et:unit -> emb_typ) (x:'a) (f:unit -> t) =
     if !Options.eager_embedding
     then f()
     else let thunk = Thunk.mk f in
-         let li = FStar.Compiler.Dyn.mkdyn x, et () in
+         let li = FStar.Dyn.mkdyn x, et () in
          mk_t <| Lazy (Inr li, thunk)
 
 let lazy_unembed (et:unit -> emb_typ) (x:t) (f:t -> option 'a) : option 'a =
@@ -295,7 +295,7 @@ let lazy_unembed (et:unit -> emb_typ) (x:t) (f:t -> option 'a) : option 'a =
                                 (show et')
            in
            res
-      else let a = FStar.Compiler.Dyn.undyn b in
+      else let a = FStar.Dyn.undyn b in
            let _ = if !Options.debug_embedding
                    then BU.print1 "Unembed cancelled for %s\n"
                                      (show (et ()))
@@ -312,7 +312,7 @@ let lazy_unembed_lazy_kind (#a:Type) (k:lazy_kind) (x:t) : option a =
   match x.nbe_t with
   | Lazy (Inl li, _) ->
     if li.lkind = k
-    then Some (FStar.Compiler.Dyn.undyn li.blob)
+    then Some (FStar.Dyn.undyn li.blob)
     else None
   | _ -> None
 
diff --git a/src/typechecker/FStar.TypeChecker.Primops.Array.fst b/src/typechecker/FStar.TypeChecker.Primops.Array.fst
index 5265b9020cd..6d23d3314a3 100644
--- a/src/typechecker/FStar.TypeChecker.Primops.Array.fst
+++ b/src/typechecker/FStar.TypeChecker.Primops.Array.fst
@@ -110,7 +110,7 @@ let ops : list primitive_step =
           (fun r universes elt_t (l, lst) ->
             //The actual primitive step computing the IA.t blob
              let blob = FStar.ImmutableArray.Base.of_list #term lst in
-             Some (universes, elt_t, (l, FStar.Compiler.Dyn.mkdyn blob))),
+             Some (universes, elt_t, (l, FStar.Dyn.mkdyn blob))),
        NBETerm.mixed_binary_op
          (fun (elt_t, _) -> Some elt_t)
          (fun (l, q) ->
@@ -128,10 +128,10 @@ let ops : list primitive_step =
                                                       [NBETerm.as_arg l]))))
          (fun  universes elt_t (l, lst) ->
             let blob = FStar.ImmutableArray.Base.of_list #NBETerm.t lst in
-            Some (universes, elt_t, (l, FStar.Compiler.Dyn.mkdyn blob))))
+            Some (universes, elt_t, (l, FStar.Dyn.mkdyn blob))))
   in
   let arg1_as_elt_t (x:arg) : option term = Some (fst x) in
-  let arg2_as_blob (x:arg) : option FStar.Compiler.Dyn.dyn =
+  let arg2_as_blob (x:arg) : option FStar.Dyn.dyn =
       //try_unembed_simple an arg as a IA.t blob if the emb_typ
       //of the lkind tells us it has the right type
       match (SS.compress (fst x)).n with
@@ -139,7 +139,7 @@ let ops : list primitive_step =
         when head=Ident.string_of_lid PC.immutable_array_t_lid -> Some blob
       | _ -> None
   in
-  let arg2_as_blob_nbe (x:NBETerm.arg) : option FStar.Compiler.Dyn.dyn =
+  let arg2_as_blob_nbe (x:NBETerm.arg) : option FStar.Dyn.dyn =
       //try_unembed_simple an arg as a IA.t blob if the emb_typ
       //tells us it has the right type
       let open FStar.TypeChecker.NBETerm in
@@ -150,8 +150,8 @@ let ops : list primitive_step =
   in
   let length_op =
     let embed_int (r:Range.range) (i:Z.t) : term = embed_simple r i in
-    let run_op (blob:FStar.Compiler.Dyn.dyn) : option Z.t =
-        Some (BU.array_length #term (FStar.Compiler.Dyn.undyn blob))
+    let run_op (blob:FStar.Dyn.dyn) : option Z.t =
+        Some (BU.array_length #term (FStar.Dyn.undyn blob))
     in
     ( PC.immutable_array_length_lid, 2, 1,
       mixed_binary_op arg1_as_elt_t //1st arg of length is the type
@@ -171,13 +171,13 @@ let ops : list primitive_step =
                         arg2_as_blob //2nd arg is the `IA.t term` blob
                         arg_as_int //3rd arg is an int
                         (fun r tm -> tm) //the result is just a term, so the embedding is the identity
-                        (fun r _universes _t blob i -> Some (BU.array_index #term (FStar.Compiler.Dyn.undyn blob) i)),
+                        (fun r _universes _t blob i -> Some (BU.array_index #term (FStar.Dyn.undyn blob) i)),
       NBETerm.mixed_ternary_op
          (fun (elt_t, _) -> Some elt_t)
          arg2_as_blob_nbe //2nd arg is an `IA.t NBEterm.t` blob
          NBETerm.arg_as_int
          (fun tm -> tm) //In this case, the result is a NBE.t, so embedding is the identity
-         (fun _universes _t blob i  -> Some (BU.array_index #NBETerm.t (FStar.Compiler.Dyn.undyn blob) i)))
+         (fun _universes _t blob i  -> Some (BU.array_index #NBETerm.t (FStar.Dyn.undyn blob) i)))
   in
   List.map (as_primitive_step true)
   [of_list_op; length_op; index_op]
diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst
index 86c38992555..b9aea01b863 100644
--- a/src/typechecker/FStar.TypeChecker.TcTerm.fst
+++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst
@@ -32,7 +32,7 @@ open FStar.Syntax.Syntax
 open FStar.Syntax.Subst
 open FStar.Syntax.Util
 open FStar.Const
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.TypeChecker.Rel
 
 open FStar.Class.Show
diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst
index 216632acd4f..89715d423ca 100644
--- a/src/typechecker/FStar.TypeChecker.Util.fst
+++ b/src/typechecker/FStar.TypeChecker.Util.fst
@@ -33,7 +33,7 @@ open FStar.Syntax.Syntax
 open FStar.Ident
 open FStar.Syntax.Subst
 open FStar.Syntax
-open FStar.Compiler.Dyn
+open FStar.Dyn
 open FStar.Class.Show
 open FStar.Class.PP
 
diff --git a/ulib/FStar.Dyn.fst b/ulib/FStar.Dyn.fst
new file mode 100644
index 00000000000..662b2717a74
--- /dev/null
+++ b/ulib/FStar.Dyn.fst
@@ -0,0 +1,41 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module FStar.Dyn
+
+// Note: this file is only a reference implementation showing that the API can
+// be implemented safely, we have a separate handcrafted ML implementation using
+// `magic`.
+// Extracting this file directly results in extra indirections, since `mkdyn`
+// would allocate a closure and `undyn` would allocate a closure and a heap
+// cell.
+
+noeq type value_type_bundle = { t: Type0; x: t }
+
+let raw_dyn (t: Type u#a) : Type0 = unit -> Dv (b:value_type_bundle {b.t == (unit -> Dv t)})
+let to_raw_dyn (#t: Type u#a) (x: t) : raw_dyn t = fun _ -> { t = unit -> Dv t; x = fun _ -> x }
+
+let dyn : Type0 = unit -> Dv value_type_bundle
+let mkdyn' (#t: Type u#a) (x: t) : dyn = to_raw_dyn x
+let dyn_has_ty (y: dyn) (t: Type u#a) = exists (x: t). y == mkdyn' x
+let mkdyn #t x = mkdyn' #t x
+
+let elim_subtype_of s (t: Type { subtype_of s t }) (x: s): t = x
+
+let undyn (#t: Type u#a) (y: dyn { dyn_has_ty y t }) : Dv t =
+  let y : raw_dyn t = elim_subtype_of _ _ y in
+  let b = y () in
+  let c : unit -> Dv t = b.x in
+  c ()
diff --git a/ulib/FStar.Dyn.fsti b/ulib/FStar.Dyn.fsti
index af46b29ff02..66b9cd89c1e 100644
--- a/ulib/FStar.Dyn.fsti
+++ b/ulib/FStar.Dyn.fsti
@@ -1,5 +1,5 @@
 (*
-   Copyright 2008-2018 Microsoft Research
+   Copyright 2008-2024 Microsoft Research
 
    Licensed under the Apache License, Version 2.0 (the "License");
    you may not use this file except in compliance with the License.
@@ -15,19 +15,17 @@
 *)
 
 module FStar.Dyn
-open FStar.All
 
-///  Dynamic casts, realized by OCaml's [Obj]
-///
-///  NOTE: THIS PROVIDES CASTS BETWEEN ARBITRARY TYPES
-///  BUT ONLY IN [False] CONTEXTS. USE WISELY.
-assume new
-type dyn 
+/// Dynamic casts
 
-(** Promoting a value of type ['a] to [dyn] *)
-val mkdyn: 'a -> EXT dyn
+val dyn : Type0
 
-(** This coerces a value of type [dyn] to any type ['a],
-    but only with [False] precondition *)
-val undyn (d: dyn{false}) : EXT 'a
+(** [dyn_has_ty d a] is true if [d] was promoted from type [a] *)
+val dyn_has_ty (d: dyn) (a: Type u#a) : prop
 
+(** Promoting a value of type [a] to [dyn] *)
+val mkdyn (#a: Type u#a) (x: a) : d:dyn { dyn_has_ty d a }
+
+(** This coerces a value of type [dyn] to its original type [a],
+    with [dyn_has_ty d a] as precondition *)
+val undyn (#a: Type u#a) (d: dyn { dyn_has_ty d a }) : Dv a