diff --git a/coq-serapi.opam b/coq-serapi.opam
index 1419cb98..b1941572 100644
--- a/coq-serapi.opam
+++ b/coq-serapi.opam
@@ -36,6 +36,7 @@ depends: [
   "ppx_hash"            {           >= "v0.13.0" & < "v0.16" }
   "yojson"              {           >= "1.7.0"               }
   "ppx_deriving_yojson" {           >= "3.4"                 }
+  "ppx_python"          {           >= "v0.15.0"             }
 ]
 
 build: [ "dune" "build" "-p" name "-j" jobs ]
diff --git a/serlib/dune b/serlib/dune
index ea8e95a0..3c29f2f3 100644
--- a/serlib/dune
+++ b/serlib/dune
@@ -2,6 +2,6 @@
  (name serlib)
  (public_name coq-serapi.serlib)
  (synopsis "Serialization Library for Coq")
- (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare ppx_deriving_yojson))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare ppx_deriving_yojson ppx_python))
  (libraries coq-core.stm sexplib))
 
diff --git a/serlib/plugins/ltac/dune b/serlib/plugins/ltac/dune
index 16d06c8a..8cc622b6 100644
--- a/serlib/plugins/ltac/dune
+++ b/serlib/plugins/ltac/dune
@@ -2,5 +2,5 @@
  (name serlib_ltac)
  (public_name coq-serapi.serlib.ltac)
  (synopsis "Serialization Library for Coq [LTAC plugin]")
- (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare ppx_python))
  (libraries coq-core.plugins.ltac serlib sexplib))
diff --git a/serlib/plugins/ltac/ser_profile_ltac.ml b/serlib/plugins/ltac/ser_profile_ltac.ml
index cb325573..66382563 100644
--- a/serlib/plugins/ltac/ser_profile_ltac.ml
+++ b/serlib/plugins/ltac/ser_profile_ltac.ml
@@ -14,9 +14,25 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
-(* XXX: Move to ser_cmap *)
-type 'a cstring_map = 'a CString.Map.t
+module String = struct
+  type t = string
+  let t_of_sexp = string_of_sexp
+  let sexp_of_t = sexp_of_string
+  let of_yojson s = Ok (Yojson.Safe.Util.to_string s)
+  let to_yojson s = `String s
+  let t_of_python = Py.String.to_string
+  let python_of_t = Py.String.of_string
+  let hash = Ppx_hash_lib.Std.Hash.Builtin.hash_string
+  let hash_fold_t = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_string
+  let compare = String.compare
+end
+
+module SM = Serlib.Ser_cMap.Make(CString.Map)(String)
+
+type 'a cstring_map = 'a SM.t
+  [@@deriving sexp,python]
 
 let from_bindings bl =
   let open CString.Map in
@@ -37,4 +53,4 @@ type treenode =
   [@with CString.Map.t   := cstring_map;
          CString.Map.key := string
   ]]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/plugins/ltac/ser_profile_ltac.mli b/serlib/plugins/ltac/ser_profile_ltac.mli
index 2dc8b7eb..75ecb7b2 100644
--- a/serlib/plugins/ltac/ser_profile_ltac.mli
+++ b/serlib/plugins/ltac/ser_profile_ltac.mli
@@ -21,3 +21,6 @@ type treenode = Profile_ltac.treenode
 
 val treenode_of_sexp : Sexp.t -> treenode
 val sexp_of_treenode : treenode -> Sexp.t
+
+val treenode_of_python : Py.Object.t -> treenode
+val python_of_treenode : treenode -> Py.Object.t
diff --git a/serlib/plugins/ltac/ser_tacenv.ml b/serlib/plugins/ltac/ser_tacenv.ml
index 94ba91f0..3d77631c 100644
--- a/serlib/plugins/ltac/ser_tacenv.ml
+++ b/serlib/plugins/ltac/ser_tacenv.ml
@@ -32,3 +32,8 @@ type ltac_entry =
   [%import: Ltac_plugin.Tacenv.ltac_entry]
   [@@deriving sexp]
 
+let ltac_entry_of_python =
+  Serlib_base.opaque_of_python ~typ:"ltac_entry"
+
+let python_of_ltac_entry =
+  Serlib_base.python_of_opaque ~typ:"ltac_entry"
diff --git a/serlib/plugins/ltac/ser_tacenv.mli b/serlib/plugins/ltac/ser_tacenv.mli
index 7cca6039..9353dd37 100644
--- a/serlib/plugins/ltac/ser_tacenv.mli
+++ b/serlib/plugins/ltac/ser_tacenv.mli
@@ -23,3 +23,6 @@ type ltac_entry = Tacenv.ltac_entry
 
 val ltac_entry_of_sexp : Sexp.t -> ltac_entry
 val sexp_of_ltac_entry : ltac_entry -> Sexp.t
+
+val ltac_entry_of_python : Py.Object.t -> ltac_entry
+val python_of_ltac_entry : ltac_entry -> Py.Object.t
diff --git a/serlib/plugins/ltac/ser_tacexpr.ml b/serlib/plugins/ltac/ser_tacexpr.ml
index 7588d692..26ddb690 100644
--- a/serlib/plugins/ltac/ser_tacexpr.ml
+++ b/serlib/plugins/ltac/ser_tacexpr.ml
@@ -678,6 +678,12 @@ and raw_atomic_tactic_expr_of_sexp tac =
     raw_tactic_expr_of_sexp
     Genarg.rlevel_of_sexp
 
+let python_of_raw_tactic_expr =
+  Serlib_base.python_of_opaque ~typ:"raw_tactic_expr"
+
+let raw_tactic_expr_of_python =
+  Serlib_base.opaque_of_python ~typ:"raw_tactic_expr"
+
 let rec sexp_of_raw_tactic_expr (tac : raw_tactic_expr) =
   sexp_of_gen_tactic_expr
     Constrexpr.sexp_of_constr_expr
diff --git a/serlib/plugins/ltac/ser_tacexpr.mli b/serlib/plugins/ltac/ser_tacexpr.mli
index 042bf9b3..07c3160c 100644
--- a/serlib/plugins/ltac/ser_tacexpr.mli
+++ b/serlib/plugins/ltac/ser_tacexpr.mli
@@ -259,7 +259,7 @@ type glob_atomic_tactic_expr = Tacexpr.glob_atomic_tactic_expr
   [@@deriving sexp,yojson,hash,compare]
 
 type raw_tactic_expr = Tacexpr.raw_tactic_expr
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,hash,compare,python]
 
 type raw_atomic_tactic_expr = Tacexpr.raw_atomic_tactic_expr
   [@@deriving sexp,yojson,hash,compare]
diff --git a/serlib/plugins/ssrmatching/dune b/serlib/plugins/ssrmatching/dune
index 83d67fef..8125ac2d 100644
--- a/serlib/plugins/ssrmatching/dune
+++ b/serlib/plugins/ssrmatching/dune
@@ -2,5 +2,5 @@
  (name serlib_ssrmatching)
  (public_name coq-serapi.serlib.ssrmatching)
  (synopsis "Serialization Library for Coq [SSR Matching plugin]")
- (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python ppx_deriving_yojson ppx_hash ppx_compare))
  (libraries coq-core.plugins.ssrmatching serlib serlib_ltac sexplib))
diff --git a/serlib/plugins/ssrmatching/ser_ssrmatching.ml b/serlib/plugins/ssrmatching/ser_ssrmatching.ml
index 04d5b1f6..954b8f6f 100644
--- a/serlib/plugins/ssrmatching/ser_ssrmatching.ml
+++ b/serlib/plugins/ssrmatching/ser_ssrmatching.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -24,22 +25,22 @@ module Geninterp = Ser_geninterp
 
 type ssrtermkind =
   [%import: Ssrmatching_plugin.Ssrmatching.ssrtermkind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cpattern =
   [%import: Ssrmatching_plugin.Ssrmatching.cpattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('a, 'b) ssrpattern =
   [%import: ('a, 'b) Ssrmatching_plugin.Ssrmatching.ssrpattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module PierceRPattern = struct
 
   type t = Ssrmatching_plugin.Ssrmatching.rpattern
 
   type _t = (cpattern, cpattern) ssrpattern
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module B_ = SerType.Pierce(PierceRPattern)
diff --git a/serlib/serType.ml b/serlib/serType.ml
index 6e97d235..ce7c565a 100644
--- a/serlib/serType.ml
+++ b/serlib/serType.ml
@@ -16,15 +16,23 @@ module type SJ = sig
   val to_yojson : t -> Yojson.Safe.t
 end
 
-module type SJH = sig
+module type SJP = sig
 
   include SJ
+  val t_of_python : Py.Object.t -> t
+  val python_of_t : t -> Py.Object.t
+
+end
+
+module type SJPH = sig
+
+  include SJP
   val hash : t -> int
   val hash_fold_t : Ppx_hash_lib.Std.Hash.state -> t -> Ppx_hash_lib.Std.Hash.state
 end
 
-module type SJHC = sig
-  include SJH
+module type SJPHC = sig
+  include SJPH
   val compare : t -> t -> int
 end
 
@@ -46,19 +54,27 @@ module type SJ1 = sig
 
 end
 
-module type SJH1 = sig
+module type SJP1 = sig
 
   include SJ1
 
+  val t_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a t
+  val python_of_t : ('a -> Py.Object.t) -> 'a t -> Py.Object.t
+end
+
+module type SJPH1 = sig
+
+  include SJP1
+
   open Ppx_hash_lib.Std.Hash
 
   val hash_fold_t : 'a folder -> 'a t folder
 
 end
 
-module type SJHC1 = sig
+module type SJPHC1 = sig
 
-  include SJH1
+  include SJPH1
 
   open Ppx_compare_lib
 
@@ -73,7 +89,7 @@ module type Bijectable = sig
   type t
 
   (* Representation type *)
-  type _t [@@deriving sexp,yojson,hash,compare]
+  type _t [@@deriving sexp,yojson,python,hash,compare]
 
   (* Need to be bijetive *)
   val to_t : _t -> t
@@ -81,13 +97,16 @@ module type Bijectable = sig
 
 end
 
-module Biject(M : Bijectable) : SJHC with type t = M.t = struct
+module Biject(M : Bijectable) : SJPHC with type t = M.t = struct
 
   type t = M.t
 
   let sexp_of_t x = M.sexp_of__t (M.of_t x)
   let t_of_sexp s = M.to_t (M._t_of_sexp s)
 
+  let python_of_t x = M.python_of__t (M.of_t x)
+  let t_of_python x = M.to_t (M._t_of_python x)
+
   let to_yojson p = M._t_to_yojson (M.of_t p)
   let of_yojson p = M._t_of_yojson p |> Result.map M.to_t
 
@@ -104,7 +123,7 @@ module type Bijectable1 = sig
   type 'a t
 
   (* Representation type *)
-  type 'a _t [@@deriving sexp,yojson,hash,compare]
+  type 'a _t [@@deriving sexp,yojson,python,hash,compare]
 
   (* Need to be bijetive *)
   val to_t : 'a _t -> 'a t
@@ -112,13 +131,16 @@ module type Bijectable1 = sig
 
 end
 
-module Biject1(M : Bijectable1) : SJHC1 with type 'a t = 'a M.t = struct
+module Biject1(M : Bijectable1) : SJPHC1 with type 'a t = 'a M.t = struct
 
   type 'a t = 'a M.t
 
   let sexp_of_t f x = M.sexp_of__t f (M.of_t x)
   let t_of_sexp f s = M.to_t (M._t_of_sexp f s)
 
+  let python_of_t f x = M.python_of__t f (M.of_t x)
+  let t_of_python f x = M.to_t (M._t_of_python f x)
+
   let to_yojson f p = M._t_to_yojson f (M.of_t p)
   let of_yojson f p = M._t_of_yojson f p |> Result.map M.to_t
 
@@ -137,7 +159,7 @@ module type Pierceable = sig
   type t
 
   (* Representation type *)
-  type _t [@@deriving sexp,yojson,hash,compare]
+  type _t [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module type Pierceable1 = sig
@@ -146,16 +168,19 @@ module type Pierceable1 = sig
   type 'a t
 
   (* Representation type *)
-  type 'a _t [@@deriving sexp,yojson,hash,compare]
+  type 'a _t [@@deriving sexp,yojson,python,hash,compare]
 end
 
-module Pierce(M : Pierceable) : SJHC with type t = M.t = struct
+module Pierce(M : Pierceable) : SJPHC with type t = M.t = struct
 
   type t = M.t
 
   let sexp_of_t x = M.sexp_of__t (_sercast x)
   let t_of_sexp s = _sercast (M._t_of_sexp s)
 
+  let python_of_t x = M.python_of__t (_sercast x)
+  let t_of_python s = _sercast (M._t_of_python s)
+
   let to_yojson p = M._t_to_yojson (_sercast p)
   let of_yojson p = M._t_of_yojson p |> Result.map _sercast
 
@@ -166,13 +191,16 @@ module Pierce(M : Pierceable) : SJHC with type t = M.t = struct
 
 end
 
-module Pierce1(M : Pierceable1) : SJHC1 with type 'a t = 'a M.t = struct
+module Pierce1(M : Pierceable1) : SJPHC1 with type 'a t = 'a M.t = struct
 
   type 'a t = 'a M.t
 
   let sexp_of_t f x = M.sexp_of__t f (_sercast x)
   let t_of_sexp f s = _sercast (M._t_of_sexp f s)
 
+  let python_of_t f x = M.python_of__t f (_sercast x)
+  let t_of_python f s = _sercast (M._t_of_python f s)
+
   let to_yojson f p = M._t_to_yojson f (_sercast p)
   let of_yojson f p = M._t_of_yojson f p |> Result.map _sercast
 
@@ -186,11 +214,14 @@ end
 (* Unfortunately this doesn't really work for types that are named as
    the functions would have to be sexp_of_name etc... Maybe fixme in
    the future *)
-module PierceAlt(M : Pierceable) : SJHC with type t := M.t = struct
+module PierceAlt(M : Pierceable) : SJPHC with type t := M.t = struct
 
   let sexp_of_t x = M.sexp_of__t (_sercast x)
   let t_of_sexp s = _sercast (M._t_of_sexp s)
 
+  let python_of_t x = M.python_of__t (_sercast x)
+  let t_of_python s = _sercast (M._t_of_python s)
+
   let to_yojson p = M._t_to_yojson (_sercast p)
   let of_yojson p = M._t_of_yojson p |> Result.map _sercast
 
@@ -203,7 +234,7 @@ end
 
 module type OpaqueDesc = sig type t val name : string end
 
-module Opaque(M : OpaqueDesc) : SJHC with type t = M.t = struct
+module Opaque(M : OpaqueDesc) : SJPHC with type t = M.t = struct
 
   type t = M.t
   let typ = M.name
@@ -211,6 +242,9 @@ module Opaque(M : OpaqueDesc) : SJHC with type t = M.t = struct
   let sexp_of_t x = Serlib_base.sexp_of_opaque ~typ x
   let t_of_sexp s = Serlib_base.opaque_of_sexp ~typ s
 
+  let python_of_t x = Serlib_base.python_of_opaque ~typ x
+  let t_of_python s = Serlib_base.opaque_of_python ~typ s
+
   let to_yojson p = Serlib_base.opaque_to_yojson ~typ p
   let of_yojson p = Serlib_base.opaque_of_yojson ~typ p
 
@@ -223,7 +257,7 @@ end
 
 module type OpaqueDesc1 = sig type 'a t val name : string end
 
-module Opaque1(M : OpaqueDesc1) : SJHC1 with type 'a t = 'a M.t = struct
+module Opaque1(M : OpaqueDesc1) : SJPHC1 with type 'a t = 'a M.t = struct
 
   type 'a  t = 'a M.t
   let typ = M.name
@@ -231,6 +265,9 @@ module Opaque1(M : OpaqueDesc1) : SJHC1 with type 'a t = 'a M.t = struct
   let sexp_of_t _ x = Serlib_base.sexp_of_opaque ~typ x
   let t_of_sexp _ s = Serlib_base.opaque_of_sexp ~typ s
 
+  let python_of_t _ x = Serlib_base.python_of_opaque ~typ x
+  let t_of_python _ s = Serlib_base.opaque_of_python ~typ s
+
   let to_yojson _ p = Serlib_base.opaque_to_yojson ~typ p
   let of_yojson _ p = Serlib_base.opaque_of_yojson ~typ p
 
diff --git a/serlib/ser_attributes.ml b/serlib/ser_attributes.ml
index 6124b640..fb34e2c5 100644
--- a/serlib/ser_attributes.ml
+++ b/serlib/ser_attributes.ml
@@ -15,15 +15,16 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module CAst = Ser_cAst
 
 type vernac_flag_type =
   [%import: Attributes.vernac_flag_type]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type vernac_flag =
   [%import: Attributes.vernac_flag]
@@ -31,4 +32,4 @@ and vernac_flag_value =
   [%import: Attributes.vernac_flag_value]
 and vernac_flags =
   [%import: Attributes.vernac_flags]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_cAst.ml b/serlib/ser_cAst.ml
index 8773d7c1..5c83cd9f 100644
--- a/serlib/ser_cAst.ml
+++ b/serlib/ser_cAst.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 module Loc        = Ser_loc
 
@@ -21,7 +22,7 @@ module L = struct
 type 'a t = {
   v   : 'a;
   loc : Loc.t option [@ignore] [@hash.ignore];
-} [@@deriving sexp,yojson,hash,compare]
+} [@@deriving sexp,yojson,python,hash,compare]
 end
 
 type 'a t = 'a CAst.t = private {
@@ -35,6 +36,9 @@ let sexp_of_t f { CAst.v ; loc } = L.sexp_of_t f { L.v ; loc }
 let of_yojson f json = Ppx_deriving_yojson_runtime.(L.of_yojson f json >|= fun { L.v; loc } -> CAst.make ?loc:loc v)
 let to_yojson f { CAst.v ; loc } = L.to_yojson f { L.v ; loc }
 
+let t_of_python f s = let { L.v ; loc } = L.t_of_python f s in CAst.make ?loc:loc v
+let python_of_t f { CAst.v ; loc } = L.python_of_t f { L.v ; loc }
+
 let hash_fold_t f st { CAst.v; loc } = L.hash_fold_t f st { L.v; loc }
 
 let compare f { CAst.v = v1; loc = l1 } { CAst.v = v2; loc = l2 } = L.compare f { L.v = v1; loc = l1 } { L.v = v2; loc = l2 }
diff --git a/serlib/ser_cAst.mli b/serlib/ser_cAst.mli
index b74e6579..334665e0 100644
--- a/serlib/ser_cAst.mli
+++ b/serlib/ser_cAst.mli
@@ -18,4 +18,7 @@ type 'a t = 'a CAst.t = private {
   loc : Loc.t option;
 } [@@deriving sexp,yojson,hash,compare]
 
+val t_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a t
+val python_of_t : ('a -> Py.Object.t) -> 'a t -> Py.Object.t
+
 val omit_att : bool ref
diff --git a/serlib/ser_cEphemeron.ml b/serlib/ser_cEphemeron.ml
index c42dd0ff..701f0e50 100644
--- a/serlib/ser_cEphemeron.ml
+++ b/serlib/ser_cEphemeron.ml
@@ -18,7 +18,7 @@ type 'a key = 'a CEphemeron.key
 module EBiject = struct
   type 'a t = 'a CEphemeron.key
 
-  type 'a _t = 'a [@@deriving sexp,yojson,hash,compare]
+  type 'a _t = 'a [@@deriving sexp,yojson,python,hash,compare]
 
   let to_t x = CEphemeron.create x
   let of_t x = CEphemeron.get x
@@ -28,6 +28,8 @@ module B = SerType.Biject1(EBiject)
 
 let sexp_of_key = B.sexp_of_t
 let key_of_sexp = B.t_of_sexp
+let python_of_key = B.python_of_t
+let key_of_python = B.t_of_python
 let key_of_yojson = B.of_yojson
 let key_to_yojson = B.to_yojson
 let hash_fold_key = B.hash_fold_t
diff --git a/serlib/ser_cMap.ml b/serlib/ser_cMap.ml
index e12e1a24..dc0c4673 100644
--- a/serlib/ser_cMap.ml
+++ b/serlib/ser_cMap.ml
@@ -17,6 +17,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -24,13 +25,11 @@ module type ExtS = sig
 
   include CSig.MapS
 
-  (* module SSet : Ser_cSet.ExtS *)
-
-  include SerType.SJHC1 with type 'a t := 'a t
+  include SerType.SJPHC1 with type 'a t := 'a t
 
 end
 
-module Make (M : CSig.MapS) (S : SerType.SJHC with type t = M.key) = struct
+module Make (M : CSig.MapS) (S : SerType.SJPHC with type t = M.key) = struct
 
   include M
 
@@ -38,7 +37,7 @@ module Make (M : CSig.MapS) (S : SerType.SJHC with type t = M.key) = struct
 
     type 'a t = 'a M.t
     type 'a _t = (S.t * 'a) list
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
     let to_t l = List.fold_left (fun e (k,s) -> M.add k s e) M.empty l
     let of_t = M.bindings
diff --git a/serlib/ser_cMap.mli b/serlib/ser_cMap.mli
index f09d76c8..9d03ad2f 100644
--- a/serlib/ser_cMap.mli
+++ b/serlib/ser_cMap.mli
@@ -20,13 +20,12 @@ module type ExtS = sig
 
   include CSig.MapS
 
-  include SerType.SJHC1 with type 'a t := 'a t
+  include SerType.SJPHC1 with type 'a t := 'a t
 
 end
 
-module Make (M : CSig.MapS) (S : SerType.SJHC with type t = M.key)
+module Make (M : CSig.MapS) (S : SerType.SJPHC with type t = M.key)
   : ExtS
     with type key = M.key
      and type 'a t = 'a M.t
      (* and module Set := M.Set *)
-
diff --git a/serlib/ser_cPrimitives.ml b/serlib/ser_cPrimitives.ml
index 186c0238..ed05d9e7 100644
--- a/serlib/ser_cPrimitives.ml
+++ b/serlib/ser_cPrimitives.ml
@@ -20,11 +20,11 @@ open Ppx_compare_lib.Builtin
 
 type t =
   [%import: CPrimitives.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type const =
   [%import: CPrimitives.const]
-  [@@deriving sexp,yojson,hash]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* XXX: GADTs ... *)
 type 'a prim_type = [%import: 'a CPrimitives.prim_type]
@@ -63,3 +63,6 @@ let op_or_type_of_sexp (x : Sexp.t) : op_or_type =
 (* XXX *)
 let op_or_type_to_yojson = Obj.magic
 let op_or_type_of_yojson = Obj.magic
+
+let python_of_op_or_type = Obj.magic
+let op_or_type_of_python = Obj.magic
diff --git a/serlib/ser_cSet.ml b/serlib/ser_cSet.ml
index d3f4de89..e88ed422 100644
--- a/serlib/ser_cSet.ml
+++ b/serlib/ser_cSet.ml
@@ -17,6 +17,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -24,11 +25,11 @@ module type ExtS = sig
 
   include CSig.SetS
 
-  include SerType.SJHC with type t := t
+  include SerType.SJPHC with type t := t
 
 end
 
-module Make (M : CSig.SetS) (S : SerType.SJHC with type t = M.elt) = struct
+module Make (M : CSig.SetS) (S : SerType.SJPHC with type t = M.elt) = struct
 
   include M
 
@@ -36,7 +37,7 @@ module Make (M : CSig.SetS) (S : SerType.SJHC with type t = M.elt) = struct
 
     type t = M.t
     type _t = S.t list
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
     let to_t = List.fold_left (fun e s -> M.add s e) M.empty
     let of_t = M.elements
diff --git a/serlib/ser_cSet.mli b/serlib/ser_cSet.mli
index 9f5a1cea..6be95e42 100644
--- a/serlib/ser_cSet.mli
+++ b/serlib/ser_cSet.mli
@@ -20,11 +20,11 @@ module type ExtS = sig
 
   include CSig.SetS
 
-  include SerType.SJHC with type t := t
+  include SerType.SJPHC with type t := t
 
 end
 
-module Make (M : CSig.SetS) (S : SerType.SJHC with type t = M.elt)
+module Make (M : CSig.SetS) (S : SerType.SJPHC with type t = M.elt)
   : ExtS
     with type t = M.t
      and type elt = M.elt
diff --git a/serlib/ser_cUnix.ml b/serlib/ser_cUnix.ml
index 55c79147..16bea04c 100644
--- a/serlib/ser_cUnix.ml
+++ b/serlib/ser_cUnix.ml
@@ -13,10 +13,11 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 type physical_path =
   [%import: CUnix.physical_path]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_constr.ml b/serlib/ser_constr.ml
index c71f9043..637b9776 100644
--- a/serlib/ser_constr.ml
+++ b/serlib/ser_constr.ml
@@ -22,6 +22,7 @@
 *)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_compare_lib.Builtin
 open Ppx_hash_lib.Std.Hash.Builtin
 
@@ -37,58 +38,58 @@ module Float64 = Ser_float64
 
 type metavariable =
   [%import: Constr.metavariable]
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type pconstant =
   [%import: Constr.pconstant]
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type pinductive =
   [%import: Constr.pinductive]
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type pconstructor =
   [%import: Constr.pconstructor]
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cast_kind =
   [%import: Constr.cast_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type case_style =
   [%import: Constr.case_style]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type case_printing =
   [%import: Constr.case_printing]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type case_info =
   [%import: Constr.case_info]
-  [@@deriving sexp,yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'constr pexistential =
   [%import: 'constr Constr.pexistential]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('constr, 'types) prec_declaration =
   [%import: ('constr, 'types) Constr.prec_declaration]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('constr, 'types) pfixpoint =
   [%import: ('constr, 'types) Constr.pfixpoint]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('constr, 'types) pcofixpoint =
   [%import: ('constr, 'types) Constr.pcofixpoint]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constr = Constr.constr
 type types  = Constr.constr
 
 type 'constr pcase_invert =
   [%import: 'constr Constr.pcase_invert]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let map_pcase_invert f = function
   | NoInvert -> NoInvert
@@ -97,13 +98,13 @@ let map_pcase_invert f = function
 
 type 'constr pcase_branch =
   [%import: 'constr Constr.pcase_branch]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let map_pcase_branch f (bi, c) = (bi, f c)
 
 type 'types pcase_return =
   [%import: 'types Constr.pcase_return]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let map_pcase_return f (bi, c) = (bi, f c)
 
@@ -128,7 +129,7 @@ type _constr =
   | Int       of Uint63.t
   | Float     of Float64.t
   | Array     of Univ.Instance.t * _constr array * _constr * _constr
-[@@deriving sexp,yojson,hash,compare]
+[@@deriving sexp,yojson,python,hash,compare]
 
 let rec _constr_put (c : constr) : _constr =
   let cr  = _constr_put           in
@@ -197,7 +198,7 @@ module ConstrBij = struct
   type t = constr
 
   type _t = _constr
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
   let to_t = _constr_get
   let of_t = _constr_put
@@ -209,6 +210,8 @@ module CC = SerType.Biject(ConstrBij)
 (* type constr = CC.t *)
 let sexp_of_constr = CC.sexp_of_t
 let constr_of_sexp = CC.t_of_sexp
+let python_of_constr = CC.python_of_t
+let constr_of_python = CC.t_of_python
 let constr_of_yojson = CC.of_yojson
 let constr_to_yojson = CC.to_yojson
 let hash_constr = CC.hash
@@ -217,6 +220,8 @@ let compare_constr = CC.compare
 
 let sexp_of_types = CC.sexp_of_t
 let types_of_sexp = CC.t_of_sexp
+let types_of_python = CC.t_of_python
+let python_of_types = CC.python_of_t
 let types_of_yojson = CC.of_yojson
 let types_to_yojson = CC.to_yojson
 let hash_types = CC.hash
@@ -227,6 +232,8 @@ type t = constr
 
 let t_of_sexp = constr_of_sexp
 let sexp_of_t = sexp_of_constr
+let t_of_python = CC.t_of_python
+let python_of_t = CC.python_of_t
 let of_yojson = constr_of_yojson
 let to_yojson = constr_to_yojson
 let hash = hash_constr
@@ -237,6 +244,7 @@ type case_invert =
   [%import: Constr.case_invert]
   [@@deriving sexp,yojson]
 
+
 type rec_declaration =
   [%import: Constr.rec_declaration]
   [@@deriving sexp]
@@ -259,16 +267,16 @@ let sexp_of_sorts_family = Sorts.sexp_of_family
 
 type named_declaration =
   [%import: Constr.named_declaration]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type named_context =
   [%import: Constr.named_context]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type rel_declaration =
   [%import: Constr.rel_declaration]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type rel_context =
   [%import: Constr.rel_context]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_constr.mli b/serlib/ser_constr.mli
index 25b12dcc..f29ca452 100644
--- a/serlib/ser_constr.mli
+++ b/serlib/ser_constr.mli
@@ -36,8 +36,8 @@ type pconstructor = Constr.pconstructor
 val pconstructor_of_sexp : Sexp.t -> pconstructor
 val sexp_of_pconstructor : pconstructor -> Sexp.t
 
-type cast_kind = Constr.cast_kind [@@deriving sexp, yojson, hash,compare]
-type case_style = Constr.case_style [@@deriving sexp, yojson, hash,compare]
+type cast_kind = Constr.cast_kind [@@deriving sexp,yojson,python,hash,compare]
+type case_style = Constr.case_style [@@deriving sexp,yojson,python,hash,compare]
 
 type case_printing = Constr.case_printing
 
@@ -65,7 +65,7 @@ val cofixpoint_of_sexp : Sexp.t -> cofixpoint
 val sexp_of_cofixpoint : cofixpoint -> Sexp.t
 
 type 'constr pexistential = 'constr Constr.pexistential
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp, yojson, python, hash, compare]
 
 type ('constr, 'types) prec_declaration = ('constr, 'types) Constr.prec_declaration
 
@@ -99,12 +99,21 @@ val sexp_of_pcofixpoint :
 type t = Constr.t
   [@@deriving sexp,yojson,hash,compare]
 
+val t_of_python : Py.Object.t -> t
+val python_of_t : t -> Py.Object.t
+
 type constr = t
   [@@deriving sexp,yojson,hash,compare]
 
+val constr_of_python : Py.Object.t -> constr
+val python_of_constr : constr -> Py.Object.t
+
 type types  = constr
   [@@deriving sexp,yojson,hash,compare]
 
+val types_of_python : Py.Object.t -> types
+val python_of_types : types -> Py.Object.t
+
 type existential = Constr.existential
 val existential_of_sexp : Sexp.t -> existential
 val sexp_of_existential : existential -> Sexp.t
@@ -116,13 +125,17 @@ val sexp_of_sorts_family : sorts_family -> Sexp.t
 type named_declaration = Constr.named_declaration
 val named_declaration_of_sexp : Sexp.t -> named_declaration
 val sexp_of_named_declaration : named_declaration -> Sexp.t
+val named_declaration_of_python : Py.Object.t -> named_declaration
+val python_of_named_declaration : named_declaration -> Py.Object.t
 
 type named_context = Constr.named_context
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type rel_declaration = Constr.rel_declaration
 val rel_declaration_of_sexp : Sexp.t -> rel_declaration
 val sexp_of_rel_declaration : rel_declaration -> Sexp.t
+val rel_declaration_of_python : Py.Object.t -> rel_declaration
+val python_of_rel_declaration : rel_declaration -> Py.Object.t
 
 type rel_context = Constr.rel_context
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_constrexpr.ml b/serlib/ser_constrexpr.ml
index b3b689ec..91b17599 100644
--- a/serlib/ser_constrexpr.ml
+++ b/serlib/ser_constrexpr.ml
@@ -13,13 +13,13 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
 let hash_fold_array = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_array_frozen
 
-open Sexplib.Std
-
 module Loc        = Ser_loc
 module CAst       = Ser_cAst
 module Names      = Ser_names
@@ -36,63 +36,63 @@ module Univ       = Ser_univ
 
 type sort_name_expr =
   [%import: Constrexpr.sort_name_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type univ_level_expr =
   [%import: Constrexpr.univ_level_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type sort_expr =
   [%import: Constrexpr.sort_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type univ_constraint_expr =
   [%import: Constrexpr.univ_constraint_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type instance_expr =
    [%import: Constrexpr.instance_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a or_by_notation_r =
   [%import: 'a Constrexpr.or_by_notation_r]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a or_by_notation =
   [%import: 'a Constrexpr.or_by_notation]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type universe_decl_expr =
   [%import: Constrexpr.universe_decl_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ident_decl =
   [%import: Constrexpr.ident_decl]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cumul_univ_decl_expr =
   [%import: Constrexpr.cumul_univ_decl_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cumul_ident_decl =
   [%import: Constrexpr.cumul_ident_decl]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type name_decl =
   [%import: Constrexpr.name_decl]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type notation_entry =
   [%import: Constrexpr.notation_entry]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type entry_level =
   [%import: Constrexpr.entry_level]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python,python]
 
 type entry_relative_level =
   [%import: Constrexpr.entry_relative_level]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python,python]
 
 type notation_entry_level =
   [%import: Constrexpr.notation_entry_level]
@@ -100,19 +100,19 @@ type notation_entry_level =
 
 type notation_key =
   [%import: Constrexpr.notation_key]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type notation =  [%import: Constrexpr.notation]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type explicitation = [%import: Constrexpr.explicitation]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type binder_kind = [%import: Constrexpr.binder_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type explicit_flag = [%import: Constrexpr.explicit_flag]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* type abstraction_kind = [%import: Constrexpr.abstraction_kind]
  *   [@@deriving sexp,yojson] *)
@@ -127,11 +127,11 @@ type explicit_flag = [%import: Constrexpr.explicit_flag]
  *   [@@deriving sexp,yojson] *)
 
 type prim_token = [%import: Constrexpr.prim_token]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type notation_with_optional_scope =
   [%import: Constrexpr.notation_with_optional_scope]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cases_pattern_expr_r = [%import: Constrexpr.cases_pattern_expr_r]
 and cases_pattern_expr = [%import: Constrexpr.cases_pattern_expr]
@@ -147,16 +147,17 @@ and recursion_order_expr_r = [%import: Constrexpr.recursion_order_expr_r]
 and recursion_order_expr = [%import: Constrexpr.recursion_order_expr]
 and local_binder_expr    = [%import: Constrexpr.local_binder_expr]
 and constr_notation_substitution = [%import: Constrexpr.constr_notation_substitution]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constr_pattern_expr = [%import: Constrexpr.constr_pattern_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type with_declaration_ast =
   [%import: Constrexpr.with_declaration_ast]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
-type module_ast_r = [%import: Constrexpr.module_ast_r]
+type module_ast_r =
+  [%import: Constrexpr.module_ast_r]
 and module_ast =
   [%import: Constrexpr.module_ast]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_constrexpr.mli b/serlib/ser_constrexpr.mli
index 4a31da8b..c0300927 100644
--- a/serlib/ser_constrexpr.mli
+++ b/serlib/ser_constrexpr.mli
@@ -15,15 +15,16 @@
 
 open Sexplib
 
-type 'a or_by_notation = 'a Constrexpr.or_by_notation [@@deriving sexp, yojson, hash,compare]
-
-type notation_entry = Constrexpr.notation_entry [@@deriving sexp, yojson, hash,compare]
+type 'a or_by_notation = 'a Constrexpr.or_by_notation [@@deriving sexp,yojson,python,hash,compare]
+type notation_entry = Constrexpr.notation_entry [@@deriving sexp,yojson,python,hash,compare]
 
 type entry_level = Constrexpr.entry_level
 val entry_level_of_sexp : Sexp.t -> entry_level
 val sexp_of_entry_level : entry_level -> Sexp.t
 val entry_level_of_yojson : Yojson.Safe.t -> (entry_level, string) Result.result
 val entry_level_to_yojson : entry_level -> Yojson.Safe.t
+val entry_level_of_python : Py.Object.t -> entry_level
+val python_of_entry_level : entry_level -> Py.Object.t
 
 type notation_entry_level = Constrexpr.notation_entry_level
 val notation_entry_level_of_sexp : Sexp.t -> notation_entry_level
@@ -36,23 +37,30 @@ val entry_relative_level_of_sexp : Sexp.t -> entry_relative_level
 val sexp_of_entry_relative_level : entry_relative_level -> Sexp.t
 val entry_relative_level_of_yojson : Yojson.Safe.t -> (entry_relative_level, string) Result.result
 val entry_relative_level_to_yojson : entry_relative_level -> Yojson.Safe.t
+val entry_relative_level_of_python : Py.Object.t -> entry_relative_level
+val python_of_entry_relative_level : entry_relative_level -> Py.Object.t
 
-type universe_decl_expr = Constrexpr.universe_decl_expr [@@deriving sexp, yojson, hash,compare]
-type ident_decl = Constrexpr.ident_decl [@@deriving sexp, yojson, hash,compare]
-type cumul_ident_decl = Constrexpr.cumul_ident_decl [@@deriving sexp, yojson, hash,compare]
-type univ_constraint_expr = Constrexpr.univ_constraint_expr [@@deriving sexp, yojson, hash,compare]
-type name_decl = Constrexpr.name_decl [@@deriving sexp, yojson, hash,compare]
+type universe_decl_expr = Constrexpr.universe_decl_expr [@@deriving sexp,yojson,python,hash,compare]
+type ident_decl = Constrexpr.ident_decl [@@deriving sexp,yojson,python,hash,compare]
+type cumul_ident_decl = Constrexpr.cumul_ident_decl [@@deriving sexp,yojson,python,hash,compare]
+type univ_constraint_expr = Constrexpr.univ_constraint_expr [@@deriving sexp,yojson,python,hash,compare]
+type name_decl = Constrexpr.name_decl [@@deriving sexp,yojson,python,hash,compare]
 
 type notation = Constrexpr.notation
 
 val notation_of_sexp : Sexp.t -> notation
 val sexp_of_notation : notation -> Sexp.t
+val notation_of_python : Py.Object.t -> notation
+val python_of_notation : notation -> Py.Object.t
 
 type explicitation = Constrexpr.explicitation
 
 val explicitation_of_sexp : Sexp.t -> explicitation
 val sexp_of_explicitation : explicitation -> Sexp.t
 
+val explicitation_of_python : Py.Object.t -> explicitation
+val python_of_explicitation : explicitation -> Py.Object.t
+
 type binder_kind = Constrexpr.binder_kind
 
 val binder_kind_of_sexp : Sexp.t -> binder_kind
@@ -95,9 +103,9 @@ and cofix_expr           = Constrexpr.cofix_expr
 and recursion_order_expr = Constrexpr.recursion_order_expr
 and local_binder_expr    = Constrexpr.local_binder_expr
 and constr_notation_substitution = Constrexpr.constr_notation_substitution
-[@@deriving sexp, yojson, hash,compare]
+[@@deriving sexp,yojson,python,hash,compare]
 
-type constr_pattern_expr = Constrexpr.constr_pattern_expr [@@deriving sexp, yojson, hash,compare]
+type constr_pattern_expr = Constrexpr.constr_pattern_expr [@@deriving sexp,yojson,python,hash,compare]
 
 type with_declaration_ast = Constrexpr.with_declaration_ast
 
@@ -106,4 +114,4 @@ val sexp_of_with_declaration_ast : with_declaration_ast -> Sexp.t
 val with_declaration_ast_of_yojson : Yojson.Safe.t -> (with_declaration_ast, string) Result.result
 val with_declaration_ast_to_yojson : with_declaration_ast -> Yojson.Safe.t
 
-type module_ast = Constrexpr.module_ast [@@deriving sexp,yojson,hash,compare]
+type module_ast = Constrexpr.module_ast [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_context.ml b/serlib/ser_context.ml
index b7410866..c3008ce7 100644
--- a/serlib/ser_context.ml
+++ b/serlib/ser_context.ml
@@ -15,6 +15,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -23,7 +24,7 @@ module Sorts   = Ser_sorts
 
 type 'a binder_annot =
   [%import: 'a Context.binder_annot]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module Rel = struct
 
@@ -31,14 +32,13 @@ module Rel = struct
 
   type ('constr, 'types) pt =
     [%import: ('constr, 'types) Context.Rel.Declaration.pt]
-    [@@deriving sexp,yojson,hash,compare]
-
+    [@@deriving sexp,yojson,python,hash,compare]
 
   end
 
   type ('constr, 'types) pt =
     [%import: ('constr, 'types) Context.Rel.pt]
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
 end
 
@@ -48,14 +48,12 @@ module Named = struct
 
   type ('constr, 'types) pt =
     [%import: ('constr, 'types) Context.Named.Declaration.pt]
-    [@@deriving sexp,yojson,hash,compare]
-
+    [@@deriving sexp,yojson,python,hash,compare]
   end
 
   type ('constr, 'types) pt =
     [%import: ('constr, 'types) Context.Named.pt]
-    [@@deriving sexp,yojson,hash,compare]
-
+    [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module Compacted = struct
@@ -64,13 +62,12 @@ module Compacted = struct
 
   type ('constr, 'types) pt =
     [%import: ('constr, 'types) Context.Compacted.Declaration.pt]
-    [@@deriving sexp]
+    [@@deriving sexp,python]
 
   end
 
   type ('constr, 'types) pt =
     [%import: ('constr, 'types) Context.Compacted.pt]
-    [@@deriving sexp]
+    [@@deriving sexp,python]
 
 end
-
diff --git a/serlib/ser_context.mli b/serlib/ser_context.mli
index b84274b3..0cddc046 100644
--- a/serlib/ser_context.mli
+++ b/serlib/ser_context.mli
@@ -17,33 +17,26 @@
 open Sexplib
 
 type 'a binder_annot = 'a Context.binder_annot
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module Rel : sig
   module Declaration : sig
-
     type ('c,'t) pt = ('c,'t) Context.Rel.Declaration.pt
-     [@@deriving sexp,yojson,hash,compare]
-
+     [@@deriving sexp,yojson,python,hash,compare]
   end
 
   type ('c, 't) pt = ('c,'t) Context.Rel.pt
-   [@@deriving sexp,yojson,hash,compare]
-
+   [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module Named : sig
-
   module Declaration : sig
-
     type ('c, 't) pt = ('c, 't) Context.Named.Declaration.pt
-     [@@deriving sexp,yojson,hash,compare]
-
+     [@@deriving sexp,yojson,python,hash,compare]
   end
 
   type ('c, 't) pt = ('c, 't) Context.Named.pt
-   [@@deriving sexp,yojson,hash,compare]
-
+   [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module Compacted : sig
diff --git a/serlib/ser_conv_oracle.ml b/serlib/ser_conv_oracle.ml
index 98c2b670..3ecc03c9 100644
--- a/serlib/ser_conv_oracle.ml
+++ b/serlib/ser_conv_oracle.ml
@@ -13,13 +13,14 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 type level =
   [%import: Conv_oracle.level]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module OpaqueOracle = struct
   type t = Conv_oracle.oracle
@@ -31,6 +32,8 @@ module B = SerType.Opaque(OpaqueOracle)
 type oracle = B.t
 let sexp_of_oracle = B.sexp_of_t
 let oracle_of_sexp = B.t_of_sexp
+let python_of_oracle = B.python_of_t
+let oracle_of_python = B.t_of_python
 let oracle_of_yojson = B.of_yojson
 let oracle_to_yojson = B.to_yojson
 let hash_oracle = B.hash
diff --git a/serlib/ser_conv_oracle.mli b/serlib/ser_conv_oracle.mli
index 4e4cce90..91162e88 100644
--- a/serlib/ser_conv_oracle.mli
+++ b/serlib/ser_conv_oracle.mli
@@ -13,5 +13,5 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-type level = Conv_oracle.level [@@deriving sexp,yojson,hash,compare]
-type oracle = Conv_oracle.oracle [@@deriving sexp,yojson,hash,compare]
+type level = Conv_oracle.level [@@deriving sexp,yojson,python,hash,compare]
+type oracle = Conv_oracle.oracle [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_cooking.ml b/serlib/ser_cooking.ml
index d031f525..f8dc5949 100644
--- a/serlib/ser_cooking.ml
+++ b/serlib/ser_cooking.ml
@@ -17,6 +17,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -28,21 +29,21 @@ type abstr_info = {
   abstr_ctx : Constr.named_context;
   abstr_auctx : Univ.AbstractContext.t;
   abstr_ausubst : Univ.Instance.t;
-} [@@deriving sexp,yojson,hash,compare]
+} [@@deriving sexp,yojson,python,hash,compare]
 
 type abstr_inst_info = {
   abstr_rev_inst : Names.Id.t list;
   abstr_uinst : Univ.Instance.t;
-} [@@deriving sexp,yojson,hash,compare]
+} [@@deriving sexp,yojson,python,hash,compare]
 
-type 'a entry_map = 'a Names.Cmap.t * 'a Names.Mindmap.t [@@deriving sexp,yojson,hash,compare]
-type expand_info = abstr_inst_info entry_map [@@deriving sexp,yojson,hash,compare]
+type 'a entry_map = 'a Names.Cmap.t * 'a Names.Mindmap.t [@@deriving sexp,yojson,python,hash,compare]
+type expand_info = abstr_inst_info entry_map [@@deriving sexp,yojson,python,hash,compare]
 
 module CIP = struct
 type _t = {
   expand_info : expand_info;
   abstr_info : abstr_info;
-} [@@deriving sexp,yojson,hash,compare]
+} [@@deriving sexp,yojson,python,hash,compare]
 
 type t =
   [%import: Cooking.cooking_info]
@@ -53,6 +54,8 @@ module B_ = SerType.Pierce(CIP)
 type cooking_info = B_.t
 let sexp_of_cooking_info = B_.sexp_of_t
 let cooking_info_of_sexp = B_.t_of_sexp
+let python_of_cooking_info = B_.python_of_t
+let cooking_info_of_python = B_.t_of_python
 let cooking_info_of_yojson = B_.of_yojson
 let cooking_info_to_yojson = B_.to_yojson
 let hash_cooking_info = B_.hash
diff --git a/serlib/ser_cooking.mli b/serlib/ser_cooking.mli
index 7e4764a9..7b2cee11 100644
--- a/serlib/ser_cooking.mli
+++ b/serlib/ser_cooking.mli
@@ -16,4 +16,4 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-type cooking_info = Cooking.cooking_info [@@deriving sexp,yojson,hash,compare]
+type cooking_info = Cooking.cooking_info [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_coqargs.ml b/serlib/ser_coqargs.ml
index dd5c75a3..9093b691 100644
--- a/serlib/ser_coqargs.ml
+++ b/serlib/ser_coqargs.ml
@@ -8,9 +8,10 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 module Names = Ser_names
 
 type top =
   [%import: Coqargs.top]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
diff --git a/serlib/ser_dAst.ml b/serlib/ser_dAst.ml
index 84428e08..c2979067 100644
--- a/serlib/ser_dAst.ml
+++ b/serlib/ser_dAst.ml
@@ -30,6 +30,14 @@ let sexp_of_thunk : type a b. (a -> Sexp.t) -> (b -> Sexp.t) -> (a,b) thunk -> S
 let thunk_of_sexp : type a b. (Sexp.t -> a) -> (Sexp.t -> b) -> Sexp.t -> (a,b) thunk =
   fun f _ s -> Value (f s)
 
+let python_of_thunk : type a b. (a -> Py.Object.t) -> (b -> Py.Object.t) -> (a,b) thunk -> Py.Object.t =
+  fun f _ t -> match t with
+  | Value v -> f v
+  | Thunk t -> f (Lazy.force t)
+
+let thunk_of_python : type a b. (Py.Object.t -> a) -> (Py.Object.t -> b) -> Py.Object.t -> (a,b) thunk =
+  fun f _ s -> Value (f s)
+
 let thunk_of_yojson : type a b. (Yojson.Safe.t -> (a, string) Result.result) -> (Yojson.Safe.t -> (b, string) Result.result) -> Yojson.Safe.t -> ((a,b) thunk, string) Result.result =
   fun f _ s -> Result.map (fun s -> Value s) (f s)
 
@@ -57,4 +65,4 @@ let compare_thunk : type a b. (a Ppx_compare_lib.compare) -> (b Ppx_compare_lib.
 
 type ('a, 'b) t =
   [%import: ('a, 'b) DAst.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_dAst.mli b/serlib/ser_dAst.mli
index 3a8780bf..c5d15bea 100644
--- a/serlib/ser_dAst.mli
+++ b/serlib/ser_dAst.mli
@@ -1,3 +1,3 @@
 type ('a, 'b) t = ('a,'b) DAst.t
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml
index 5b4df668..27795c33 100644
--- a/serlib/ser_declarations.ml
+++ b/serlib/ser_declarations.ml
@@ -15,8 +15,13 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
+
+(* let python_of_unit _ = Py.Int.of_int 0
+ * let unit_of_python _ = () *)
+
 let hash_fold_array = hash_fold_array_frozen
 
 module Rtree   = Ser_rtree
@@ -35,36 +40,36 @@ module Retroknowledge = Ser_retroknowledge
 
 type template_arity =
   [%import: Declarations.template_arity]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('a, 'b) declaration_arity =
   [%import: ('a, 'b) Declarations.declaration_arity]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type nested_type =
   [%import: Declarations.nested_type]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type recarg =
   [%import: Declarations.recarg]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type wf_paths =
   [%import: Declarations.wf_paths]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type regular_inductive_arity =
   [%import: Declarations.regular_inductive_arity
   [@with Term.sorts := Sorts.t;]]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type inductive_arity =
   [%import: Declarations.inductive_arity]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type one_inductive_body =
   [%import: Declarations.one_inductive_body]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* type set_predicativity =
  *   [%import: Declarations.set_predicativity]
@@ -76,19 +81,19 @@ type one_inductive_body =
 
 type inline =
   [%import: Declarations.inline]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type universes =
   [%import: Declarations.universes]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('a, 'b) constant_def =
   [%import: ('a, 'b) Declarations.constant_def]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type typing_flags =
   [%import: Declarations.typing_flags]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* type work_list =
  *   [%import: Declarations.work_list]
@@ -104,11 +109,11 @@ type typing_flags =
 
 type 'a pconstant_body =
   [%import: 'a Declarations.pconstant_body]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constant_body =
   [%import: Declarations.constant_body]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let sexp_of_constant_body e =
   (* We cannot handle VM values *)
@@ -124,6 +129,8 @@ module B_ = SerType.Opaque1(MRK)
 type 'a module_retroknowledge = 'a B_.t
 let sexp_of_module_retroknowledge = B_.sexp_of_t
 let module_retroknowledge_of_sexp = B_.t_of_sexp
+let _python_of_module_retroknowledge = B_.python_of_t
+let _module_retroknowledge_of_python = B_.t_of_python
 let module_retroknowledge_of_yojson = B_.of_yojson
 let module_retroknowledge_to_yojson = B_.to_yojson
 let hash_fold_module_retroknowledge = B_.hash_fold_t
@@ -131,32 +138,32 @@ let compare_module_retroknowledge = B_.compare
 
 type recursivity_kind =
   [%import: Declarations.recursivity_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type record_info =
   [%import: Declarations.record_info]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type template_universes =
   [%import: Declarations.template_universes]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type mutual_inductive_body =
   [%import: Declarations.mutual_inductive_body
   [@with Context.section_context := Context.Named.t;]]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('ty,'a) functorize =
   [%import: ('ty, 'a) Declarations.functorize]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a with_declaration =
   [%import: 'a Declarations.with_declaration]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a module_alg_expr =
   [%import: 'a Declarations.module_alg_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type structure_field_body =
   [%import: Declarations.structure_field_body]
@@ -189,3 +196,10 @@ and module_body =
 and module_type_body =
   [%import: Declarations.module_type_body]
   [@@deriving sexp,yojson,hash,compare]
+
+let structure_body_of_python = Obj.magic 0
+let python_of_structure_body = Obj.magic 0
+let module_body_of_python = Obj.magic 0
+let python_of_module_body = Obj.magic 0
+let module_type_body_of_python = Obj.magic 0
+let python_of_module_type_body = Obj.magic 0
diff --git a/serlib/ser_declarations.mli b/serlib/ser_declarations.mli
index 6992f286..cd1b4ff0 100644
--- a/serlib/ser_declarations.mli
+++ b/serlib/ser_declarations.mli
@@ -52,40 +52,18 @@ type one_inductive_body = Declarations.one_inductive_body
 val one_inductive_body_of_sexp : Sexp.t -> one_inductive_body
 val sexp_of_one_inductive_body : one_inductive_body -> Sexp.t
 
-(* type set_predicativity = Declarations.set_predicativity
- * val set_predicativity_of_sexp : Sexp.t -> set_predicativity
- * val sexp_of_set_predicativity : set_predicativity -> Sexp.t *)
-
-(* type engagement = Declarations.engagement
- * val engagement_of_sexp : Sexp.t -> engagement
- * val sexp_of_engagement : engagement -> Sexp.t *)
-
 type typing_flags = Declarations.typing_flags
 val typing_flags_of_sexp : Sexp.t -> typing_flags
 val sexp_of_typing_flags : typing_flags -> Sexp.t
+val typing_flags_of_python : Py.Object.t -> typing_flags
+val python_of_typing_flags : typing_flags -> Py.Object.t
 
 type inline = Declarations.inline
 val sexp_of_inline : inline -> Sexp.t
 val inline_of_sexp : Sexp.t -> inline
 
-(* type work_list = Declarations.work_list *)
-
-(* type abstr_info = Declarations.abstr_info = {
- *   abstr_ctx : Constr.named_context;
- *   abstr_subst : Univ.Instance.t;
- *   abstr_uctx : Univ.AbstractContext.t;
- * }
- * 
- * type cooking_info = Declarations.cooking_info
- * val sexp_of_cooking_info : cooking_info -> Sexp.t
- * val cooking_info_of_sexp : Sexp.t -> cooking_info *)
-
 type constant_body = Declarations.constant_body
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type record_body = Declarations.record_body
- * val record_body_of_sexp : Sexp.t -> record_body
- * val sexp_of_record_body : record_body -> Sexp.t *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type recursivity_kind = Declarations.recursivity_kind
 val recursivity_kind_of_sexp : Sexp.t -> recursivity_kind
@@ -94,17 +72,17 @@ val recursivity_kind_of_yojson : Yojson.Safe.t -> (recursivity_kind, string) Res
 val recursivity_kind_to_yojson : recursivity_kind -> Yojson.Safe.t
 
 type mutual_inductive_body = Declarations.mutual_inductive_body
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a module_alg_expr = 'a Declarations.module_alg_expr
 val sexp_of_module_alg_expr : ('a -> Sexp.t) -> 'a module_alg_expr -> Sexp.t
 val module_alg_expr_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a module_alg_expr
 
 type structure_body = Declarations.structure_body
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type module_body = Declarations.module_body
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type module_type_body = Declarations.module_type_body
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_declaremods.ml b/serlib/ser_declaremods.ml
index a5571e25..4b66c85c 100644
--- a/serlib/ser_declaremods.ml
+++ b/serlib/ser_declaremods.ml
@@ -15,14 +15,15 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Conv
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
 
 type 'a module_signature =
   [%import: 'a Declaremods.module_signature]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type inline =
   [%import: Declaremods.inline]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_declaremods.mli b/serlib/ser_declaremods.mli
index 20065b04..3d35ce09 100644
--- a/serlib/ser_declaremods.mli
+++ b/serlib/ser_declaremods.mli
@@ -15,5 +15,5 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-type 'a module_signature = 'a Declaremods.module_signature [@@deriving sexp,yojson,hash,compare]
-type inline = Declaremods.inline [@@deriving sexp,yojson,hash,compare]
+type 'a module_signature = 'a Declaremods.module_signature [@@deriving sexp,yojson,python,hash,compare]
+type inline = Declaremods.inline [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_decls.ml b/serlib/ser_decls.ml
index b2457766..911623d5 100644
--- a/serlib/ser_decls.ml
+++ b/serlib/ser_decls.ml
@@ -15,16 +15,16 @@
 
 type definition_object_kind =
   [%import: Decls.definition_object_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type theorem_kind =
   [%import: Decls.theorem_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type assumption_object_kind =
   [%import: Decls.assumption_object_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type logical_kind =
   [%import: Decls.logical_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_eConstr.ml b/serlib/ser_eConstr.ml
index 9ba96aa7..0de53915 100644
--- a/serlib/ser_eConstr.ml
+++ b/serlib/ser_eConstr.ml
@@ -24,7 +24,7 @@ module ECtoC = struct
 
   type t = EConstr.t
   type _t = Constr.t
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
   let to_t = EConstr.of_constr
   let of_t = EConstr.Unsafe.to_constr
diff --git a/serlib/ser_environ.ml b/serlib/ser_environ.ml
index 6758aa66..dfa756e6 100644
--- a/serlib/ser_environ.ml
+++ b/serlib/ser_environ.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -31,50 +32,48 @@ module Declarations   = Ser_declarations
 
 type lazy_val = [%import: Environ.lazy_val]
 let sexp_of_lazy_val = Serlib_base.sexp_of_opaque ~typ:"Environ.lazy_val"
-
-(* type stratification =
- *   [%import: Environ.stratification]
- *   [@@deriving sexp_of] *)
+let python_of_lazy_val = Serlib_base.python_of_opaque ~typ:"Environ.lazy_val"
 
 type rel_context_val =
   [%import: Environ.rel_context_val]
-  [@@deriving sexp_of]
+  [@@deriving sexp_of,python_of]
 
 type named_context_val =
   [%import: Environ.named_context_val]
-  [@@deriving sexp_of]
+  [@@deriving sexp_of,python_of]
 
 type link_info =
   [%import: Environ.link_info]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type key =
   [%import: Environ.key]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constant_key =
   [%import: Environ.constant_key]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type mind_key =
   [%import: Environ.mind_key]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module Globals = struct
 
   module PierceSpec = struct
     type t = Environ.Globals.t
     type _t = [%import: Environ.Globals.view]
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
   end
   include SerType.Pierce(PierceSpec)
 end
 
 type env =
   [%import: Environ.env]
-  [@@deriving sexp_of]
+  [@@deriving sexp_of, python_of]
 
 let env_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Environ.env"
+let env_of_python = Serlib_base.opaque_of_python ~typ:"Environ.env"
 
 let abstract_env = ref false
 let sexp_of_env env =
diff --git a/serlib/ser_environ.mli b/serlib/ser_environ.mli
index ace7c296..594779a8 100644
--- a/serlib/ser_environ.mli
+++ b/serlib/ser_environ.mli
@@ -24,8 +24,10 @@ type env = Environ.env
 
 val env_of_sexp : Sexp.t -> env val sexp_of_env : env -> Sexp.t
 
-type ('constr, 'types) punsafe_judgment = ('constr, 'types)
-   Environ.punsafe_judgment
+val env_of_python : Py.Object.t -> env
+val python_of_env : env -> Py.Object.t
+
+type ('constr, 'types) punsafe_judgment = ('constr, 'types) Environ.punsafe_judgment
 
 val punsafe_judgment_of_sexp : (Sexp.t -> 'constr) -> (Sexp.t ->
    'types) -> Sexp.t -> ('constr, 'types) punsafe_judgment val
diff --git a/serlib/ser_evar.ml b/serlib/ser_evar.ml
index f6ebd567..cacdf7e0 100644
--- a/serlib/ser_evar.ml
+++ b/serlib/ser_evar.ml
@@ -14,31 +14,20 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 (* Private *)
-module Self = struct
-type t = [%import: Evar.t]
-
-type _t                    = Ser_Evar of int [@@deriving sexp,yojson,hash,compare]
-let _t_put  evar           = Ser_Evar (Evar.repr evar)
-let _t_get (Ser_Evar evar) = Evar.unsafe_of_int evar
-
-let t_of_sexp sexp = _t_get (_t_of_sexp sexp)
-let sexp_of_t evar = sexp_of__t (_t_put evar)
-
-let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get)
-let to_yojson level = _t_to_yojson (_t_put level)
-
-let hash x = hash__t (_t_put x)
-let hash_fold_t st id = hash_fold__t st (_t_put id)
-
-let compare x y = compare__t (_t_put x) (_t_put y)
+module EBi = struct
+  type t = Evar.t
+  type _t = Ser_Evar of int [@@deriving sexp,yojson,python,hash,compare]
 
+  let of_t evar = Ser_Evar (Evar.repr evar)
+  let to_t (Ser_Evar evar) = Evar.unsafe_of_int evar
 end
 
+module Self = SerType.Biject(EBi)
 include Self
-
 module Set = Ser_cSet.Make(Evar.Set)(Self)
diff --git a/serlib/ser_evar.mli b/serlib/ser_evar.mli
index 0401d704..14fd51e0 100644
--- a/serlib/ser_evar.mli
+++ b/serlib/ser_evar.mli
@@ -14,7 +14,7 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-module Self : SerType.SJHC with type t = Evar.t
+module Self : SerType.SJPHC with type t = Evar.t
 
 include module type of Self
 
diff --git a/serlib/ser_evar_kinds.ml b/serlib/ser_evar_kinds.ml
index ec32ca5c..9b148d22 100644
--- a/serlib/ser_evar_kinds.ml
+++ b/serlib/ser_evar_kinds.ml
@@ -13,9 +13,10 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module Names     = Ser_names
 module Evar      = Ser_evar
@@ -27,25 +28,24 @@ module Constr    = Ser_constr
 
 type matching_var_kind =
   [%import: Evar_kinds.matching_var_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type obligation_definition_status =
   [%import: Evar_kinds.obligation_definition_status]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type record_field =
   [%import: Evar_kinds.record_field]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type question_mark =
   [%import: Evar_kinds.question_mark]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type subevar_kind =
   [%import: Evar_kinds.subevar_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type t =
   [%import: Evar_kinds.t]
-  [@@deriving sexp,yojson,hash,compare]
-
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_evar_kinds.mli b/serlib/ser_evar_kinds.mli
index 38bb8b1d..9a3e254e 100644
--- a/serlib/ser_evar_kinds.mli
+++ b/serlib/ser_evar_kinds.mli
@@ -19,11 +19,11 @@ open Sexplib
 (* Evar_kinds.mli                                                       *)
 (************************************************************************)
 type matching_var_kind = Evar_kinds.matching_var_kind
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type obligation_definition_status = Evar_kinds.obligation_definition_status
 
 val obligation_definition_status_of_sexp : Sexp.t -> obligation_definition_status
 val sexp_of_obligation_definition_status : obligation_definition_status -> Sexp.t
 
-include SerType.SJHC with type t = Evar_kinds.t
+include SerType.SJPHC with type t = Evar_kinds.t
diff --git a/serlib/ser_extend.ml b/serlib/ser_extend.ml
index 80ae4f1d..f6750c7e 100644
--- a/serlib/ser_extend.ml
+++ b/serlib/ser_extend.ml
@@ -13,9 +13,10 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module Tok           = Ser_tok
 module Notation_term = Ser_notation_term
@@ -24,33 +25,33 @@ module Gramlib       = Ser_gramlib
 
 type side =
   [%import: Extend.side]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type production_position =
   [%import: Extend.production_position]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type production_level =
   [%import: Extend.production_level]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type binder_entry_kind =
   [%import: Extend.binder_entry_kind]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type 'lev constr_entry_key_gen =
   [%import: 'lev Extend.constr_entry_key_gen]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constr_entry_key =
   [%import: Extend.constr_entry_key]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constr_prod_entry_key =
   [%import: Extend.constr_prod_entry_key]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type simple_constr_prod_entry_key =
   [%import: Extend.simple_constr_prod_entry_key]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
diff --git a/serlib/ser_extend.mli b/serlib/ser_extend.mli
index 264ef515..82fb4cba 100644
--- a/serlib/ser_extend.mli
+++ b/serlib/ser_extend.mli
@@ -18,12 +18,14 @@ open Sexplib
 type side = Extend.side
 val side_of_sexp : Sexp.t -> side
 val sexp_of_side : side -> Sexp.t
+val side_of_python : Py.Object.t -> side
+val python_of_side : side -> Py.Object.t
 
 type production_position = Extend.production_position
 val production_position_of_sexp : Sexp.t -> production_position
 val sexp_of_production_position : production_position -> Sexp.t
 
-type production_level = Extend.production_level [@@deriving sexp,yojson,hash,compare]
+type production_level = Extend.production_level [@@deriving sexp,yojson,python,hash,compare]
 
 type binder_entry_kind = Extend.binder_entry_kind
 val binder_entry_kind_of_sexp : Sexp.t -> binder_entry_kind
@@ -38,9 +40,13 @@ val sexp_of_constr_entry_key_gen : ('lev -> Sexp.t) ->
 type constr_entry_key = Extend.constr_entry_key
 val constr_entry_key_of_sexp : Sexp.t -> constr_entry_key
 val sexp_of_constr_entry_key : constr_entry_key -> Sexp.t
+val constr_entry_key_of_python : Py.Object.t -> constr_entry_key
+val python_of_constr_entry_key : constr_entry_key -> Py.Object.t
 
 type constr_prod_entry_key = Extend.constr_prod_entry_key
 val constr_prod_entry_key_of_sexp : Sexp.t -> constr_prod_entry_key
 val sexp_of_constr_prod_entry_key : constr_prod_entry_key -> Sexp.t
+val constr_prod_entry_key_of_python : Py.Object.t -> constr_prod_entry_key
+val python_of_constr_prod_entry_key : constr_prod_entry_key -> Py.Object.t
 
-type simple_constr_prod_entry_key = Extend.simple_constr_prod_entry_key [@@deriving sexp,yojson,hash,compare]
+type simple_constr_prod_entry_key = Extend.simple_constr_prod_entry_key [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_feedback.ml b/serlib/ser_feedback.ml
index a1df41ba..0719de76 100644
--- a/serlib/ser_feedback.ml
+++ b/serlib/ser_feedback.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 module Loc = Ser_loc
 
@@ -23,15 +24,15 @@ module Stateid      = Ser_stateid
 
 type level =
   [%import: Feedback.level]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp, yojson, python]
 
 type route_id =
   [%import: Feedback.route_id]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp, yojson, python]
 
 type doc_id =
   [%import: Feedback.doc_id]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp, yojson, python]
 
 type feedback_content =
   [%import: Feedback.feedback_content]
diff --git a/serlib/ser_feedback.mli b/serlib/ser_feedback.mli
index 18169f60..dd3024d7 100644
--- a/serlib/ser_feedback.mli
+++ b/serlib/ser_feedback.mli
@@ -21,6 +21,8 @@ val doc_id_of_sexp : Sexp.t -> doc_id
 val sexp_of_doc_id : doc_id -> Sexp.t
 val doc_id_of_yojson : Yojson.Safe.t -> (doc_id, string) Result.result
 val doc_id_to_yojson : doc_id -> Yojson.Safe.t
+val doc_id_of_python : Py.Object.t -> doc_id
+val python_of_doc_id : doc_id -> Py.Object.t
 
 type level = Feedback.level
 
@@ -28,12 +30,16 @@ val level_of_sexp : Sexp.t -> level
 val sexp_of_level : level -> Sexp.t
 val level_of_yojson : Yojson.Safe.t -> (level, string) Result.result
 val level_to_yojson : level -> Yojson.Safe.t
+val level_of_python : Py.Object.t -> level
+val python_of_level : level -> Py.Object.t
 
 type route_id = Feedback.route_id
 val route_id_of_sexp : Sexp.t -> route_id
 val sexp_of_route_id : route_id -> Sexp.t
 val route_id_of_yojson : Yojson.Safe.t -> (route_id, string) Result.result
 val route_id_to_yojson : route_id -> Yojson.Safe.t
+val route_id_of_python : Py.Object.t -> route_id
+val python_of_route_id : route_id -> Py.Object.t
 
 type feedback_content = Feedback.feedback_content
 
diff --git a/serlib/ser_float64.ml b/serlib/ser_float64.ml
index fbbac8c9..a4ec9985 100644
--- a/serlib/ser_float64.ml
+++ b/serlib/ser_float64.ml
@@ -17,12 +17,13 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
 module PierceSpec = struct
   type t = Float64.t
-  type _t = float [@@deriving sexp,yojson,hash,compare]
+  type _t = float [@@deriving sexp,yojson,python,hash,compare]
 end
 
 include SerType.Pierce(PierceSpec)
diff --git a/serlib/ser_future.ml b/serlib/ser_future.ml
index 605e1aca..a1ea3f6b 100644
--- a/serlib/ser_future.ml
+++ b/serlib/ser_future.ml
@@ -2,3 +2,6 @@ type 'a computation = 'a Future.computation
 
 let computation_of_sexp f x = Future.from_val (f x)
 let sexp_of_computation f x = f Future.(force x)
+let computation_of_python f x = Future.from_val (f x)
+let python_of_computation f x = f Future.(force x)
+
diff --git a/serlib/ser_genarg.ml b/serlib/ser_genarg.ml
index ec456309..664dc2ea 100644
--- a/serlib/ser_genarg.ml
+++ b/serlib/ser_genarg.ml
@@ -28,13 +28,13 @@ open Genarg
 
 type rlevel =
   [%import: Genarg.rlevel]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 type glevel =
   [%import: Genarg.glevel]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 type tlevel =
   [%import: Genarg.tlevel]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let rec sexp_of_genarg_type : type a b c. (a, b, c) genarg_type -> Sexp.t = fun gt ->
   match gt with
@@ -286,22 +286,29 @@ let generic_argument_of_sexp _lvl sexp : 'a Genarg.generic_argument =
   let (RG ga) = gen_abstype_of_sexp sexp in
   Obj.magic ga
 
-let generic_argument_of_yojson _lvl _json = Error "not supported generic_argument_of_yojson"
-let generic_argument_to_yojson _lvl _g = `String "foo"
+let generic_argument_of_yojson _lvl _json =
+  Error "not supported generic_argument_of_yojson"
+let generic_argument_to_yojson _lvl _g =
+  `String "foo"
+
+let generic_argument_of_python _ =
+  Serlib_base.opaque_of_python ~typ:"generic_argument"
+let python_of_generic_argument _ =
+  Serlib_base.python_of_opaque ~typ:"generic_argument"
 
 type 'a generic_argument = 'a Genarg.generic_argument
 
 type glob_generic_argument =
   [%import: Genarg.glob_generic_argument]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type raw_generic_argument =
   [%import: Genarg.raw_generic_argument]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type typed_generic_argument =
   [%import: Genarg.typed_generic_argument]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let mk_uniform pin pout phash pcompare =
   { raw_ser = pin
diff --git a/serlib/ser_genarg.mli b/serlib/ser_genarg.mli
index 58bbf85a..c9c546e7 100644
--- a/serlib/ser_genarg.mli
+++ b/serlib/ser_genarg.mli
@@ -30,13 +30,13 @@ type tlevel = Genarg.tlevel
   [@@deriving sexp,yojson,hash,compare]
 
 type 'a generic_argument = 'a Genarg.generic_argument
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_generic_argument = Genarg.glob_generic_argument
-[@@deriving sexp,yojson,hash,compare]
+[@@deriving sexp,yojson,python,hash,compare]
 
 type raw_generic_argument = Genarg.raw_generic_argument
-[@@deriving sexp,yojson,hash,compare]
+[@@deriving sexp,yojson,python,hash,compare]
 
 type typed_generic_argument = Genarg.typed_generic_argument
 val typed_generic_argument_of_sexp : Sexp.t -> Genarg.typed_generic_argument
diff --git a/serlib/ser_genintern.ml b/serlib/ser_genintern.ml
index 74301b63..b8c624fa 100644
--- a/serlib/ser_genintern.ml
+++ b/serlib/ser_genintern.ml
@@ -16,6 +16,7 @@
 (************************************************************************)
 
 open Sexplib.Conv
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -37,7 +38,7 @@ end
 
 type intern_variable_status =
   [%import: Genintern.intern_variable_status]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_sign =
   [%import: Genintern.glob_sign]
@@ -45,8 +46,8 @@ type glob_sign =
 
 type glob_constr_and_expr =
   [%import: Genintern.glob_constr_and_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_constr_pattern_and_expr =
   [%import: Genintern.glob_constr_pattern_and_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_genintern.mli b/serlib/ser_genintern.mli
index 92c8c646..48795fe0 100644
--- a/serlib/ser_genintern.mli
+++ b/serlib/ser_genintern.mli
@@ -17,10 +17,10 @@
 
 open Sexplib
 
-module Store : SerType.SJHC with type t = Genintern.Store.t
+module Store : SerType.SJPHC with type t = Genintern.Store.t
 
 type intern_variable_status = Genintern.intern_variable_status
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_sign = Genintern.glob_sign
 
@@ -28,7 +28,7 @@ val glob_sign_of_sexp : Sexp.t -> glob_sign
 val sexp_of_glob_sign : glob_sign -> Sexp.t
 
 type glob_constr_and_expr = Genintern.glob_constr_and_expr
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_constr_pattern_and_expr = Genintern.glob_constr_pattern_and_expr
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_geninterp.ml b/serlib/ser_geninterp.ml
index 5ab14761..ee9e06a7 100644
--- a/serlib/ser_geninterp.ml
+++ b/serlib/ser_geninterp.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Conv
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -26,12 +27,15 @@ module Val = struct
 
   (* let typ_of_sexp _ _ = Serlib_base.opaque_of_sexp "Geninterp.Val.typ" *)
   let sexp_of_typ _ x = Serlib_base.sexp_of_opaque ~typ:"Geninterp.Val.typ" x
+  let _python_of_typ _ x = Serlib_base.python_of_opaque ~typ:"Geninterp.Val.typ" x
 
   type t =
     [%import: Geninterp.Val.t]
     [@@deriving sexp_of]
 
   let t_of_sexp x = Serlib_base.opaque_of_sexp ~typ:"Geninterp.Val.t" x
+  let python_of_t x = Serlib_base.python_of_opaque ~typ:"Geninterp.Val.t" x
+  let t_of_python x = Serlib_base.opaque_of_python ~typ:"Geninterp.Val.t" x
   let of_yojson = Serlib_base.opaque_of_yojson ~typ:"Geninterp.Val.t"
   let to_yojson x = Serlib_base.opaque_to_yojson ~typ:"Geninterp.Val.t" x
 
@@ -45,6 +49,8 @@ module TacStore = struct
   type t = Geninterp.TacStore.t
   let t_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Geninterp.TacStore.t"
   let sexp_of_t = Serlib_base.sexp_of_opaque ~typ:"Geninterp.TacStore.t"
+  let t_of_python = Serlib_base.opaque_of_python ~typ:"Geninterp.TacStore.t"
+  let python_of_t = Serlib_base.python_of_opaque ~typ:"Geninterp.TacStore.t"
   let to_yojson = Serlib_base.opaque_to_yojson ~typ:"Geninterp.TacStore.t"
   let of_yojson = Serlib_base.opaque_of_yojson ~typ:"Geninterp.TacStore.t"
   let _hash = Hashtbl.hash
@@ -54,4 +60,4 @@ end
 
 type interp_sign =
   [%import: Geninterp.interp_sign]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_geninterp.mli b/serlib/ser_geninterp.mli
index b8d916a0..8a8b9fcd 100644
--- a/serlib/ser_geninterp.mli
+++ b/serlib/ser_geninterp.mli
@@ -16,9 +16,9 @@
 module Val : sig
 
   type t = Geninterp.Val.t
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 end
 
 type interp_sign = Geninterp.interp_sign
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_genredexpr.ml b/serlib/ser_genredexpr.ml
index ec6d2aef..ea603d0f 100644
--- a/serlib/ser_genredexpr.ml
+++ b/serlib/ser_genredexpr.ml
@@ -13,9 +13,10 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module Loc   = Ser_loc
 module Names = Ser_names
@@ -30,40 +31,40 @@ type 'a red_atom =
 
 type 'a glob_red_flag =
   [%import: 'a Genredexpr.glob_red_flag]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('a,'b,'c,'d) red_expr_gen0 =
   [%import: ('a,'b,'c,'d) Genredexpr.red_expr_gen0]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('a,'b,'c) red_expr_gen =
   [%import: ('a,'b,'c) Genredexpr.red_expr_gen]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('a,'b,'c) may_eval =
   [%import: ('a,'b,'c) Genredexpr.may_eval]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* Helpers for raw_red_expr *)
 type r_trm =
   [%import: Genredexpr.r_trm]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type r_cst =
   [%import: Genredexpr.r_cst]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type r_pat =
   [%import: Genredexpr.r_pat]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type raw_red_expr =
   [%import: Genredexpr.raw_red_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a and_short_name =
   [%import: 'a Genredexpr.and_short_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module A = struct
 
@@ -71,7 +72,7 @@ module A = struct
     (Ser_constrexpr.constr_expr,
      Ser_libnames.qualid Ser_constrexpr.or_by_notation,
      Ser_constrexpr.constr_expr) red_expr_gen
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
   type glb =
     (Ser_genintern.glob_constr_and_expr,
diff --git a/serlib/ser_genredexpr.mli b/serlib/ser_genredexpr.mli
index b1eafac5..e6e9f284 100644
--- a/serlib/ser_genredexpr.mli
+++ b/serlib/ser_genredexpr.mli
@@ -33,7 +33,7 @@ type ('a, 'b, 'c) red_expr_gen =  ('a, 'b, 'c) Genredexpr.red_expr_gen
 type ('a, 'b, 'c) may_eval =  ('a, 'b, 'c) Genredexpr.may_eval
   [@@deriving sexp,yojson,hash,compare]
 
-type raw_red_expr = Genredexpr.raw_red_expr [@@deriving sexp,yojson,hash,compare]
+type raw_red_expr = Genredexpr.raw_red_expr [@@deriving sexp,yojson,python,hash,compare]
 
 type r_cst = Genredexpr.r_cst
   [@@deriving sexp,yojson,hash,compare]
diff --git a/serlib/ser_glob_term.ml b/serlib/ser_glob_term.ml
index a4b7590e..0603ee13 100644
--- a/serlib/ser_glob_term.ml
+++ b/serlib/ser_glob_term.ml
@@ -13,9 +13,10 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 let hash_fold_array = hash_fold_array_frozen
 
@@ -38,67 +39,47 @@ module Namegen    = Ser_namegen
 
 type binding_kind =
   [%import: Glob_term.binding_kind]
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type 'a universe_kind =
- *   [%import: 'a Glob_term.universe_kind]
- *   [@@deriving sexp,yojson] *)
-
-(* type level_info =
- *   [%import: Glob_term.level_info]
- *   [@@deriving sexp,yojson] *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_sort_name =
   [%import: Glob_term.glob_sort_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a glob_sort_gen =
   [%import: 'a Glob_term.glob_sort_gen]
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type 'a glob_sort_expr =
- *   [%import: 'a Glob_term.glob_sort_expr]
- *   [@@deriving sexp,yojson] *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_level =
   [%import: Glob_term.glob_level]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_constraint =
   [%import: Glob_term.glob_constraint]
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type sort_info =
- *   [%import: Glob_term.sort_info]
- *   [@@deriving sexp,yojson] *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_sort =
   [%import: Glob_term.glob_sort]
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type 'a cast_type =
- *   [%import: 'a Glob_term.cast_type]
- *   [@@deriving sexp,yojson] *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type existential_name =
   [%import: Glob_term.existential_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a cases_pattern_r = [%import: 'a Glob_term.cases_pattern_r]
 and 'a cases_pattern_g  = [%import: 'a Glob_term.cases_pattern_g]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cases_pattern =
   [%import: Glob_term.cases_pattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_recarg =
   [%import: Glob_term.glob_recarg]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_fix_kind =
   [%import: Glob_term.glob_fix_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 [@@@ocaml.warning "-27"]
 type 'a glob_constr_r        = [%import: 'a Glob_term.glob_constr_r]
@@ -109,29 +90,29 @@ and 'a tomatch_tuple_g       = [%import: 'a Glob_term.tomatch_tuple_g]
 and 'a tomatch_tuples_g      = [%import: 'a Glob_term.tomatch_tuples_g]
 and 'a cases_clause_g        = [%import: 'a Glob_term.cases_clause_g]
 and 'a cases_clauses_g       = [%import: 'a Glob_term.cases_clauses_g]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 [@@@ocaml.warning "+27"]
 
 type glob_constr =
   [%import: Glob_term.glob_constr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_decl =
   [%import: Glob_term.glob_decl]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type predicate_pattern   = [%import: Glob_term.predicate_pattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type tomatch_tuple       = [%import: Glob_term.tomatch_tuple]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type tomatch_tuples      = [%import: Glob_term.tomatch_tuples]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cases_clause        = [%import: Glob_term.cases_clause]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cases_clauses       = [%import: Glob_term.cases_clauses]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
diff --git a/serlib/ser_glob_term.mli b/serlib/ser_glob_term.mli
index de8f36f9..ceee3b08 100644
--- a/serlib/ser_glob_term.mli
+++ b/serlib/ser_glob_term.mli
@@ -15,8 +15,8 @@
 
 open Sexplib
 
-type binding_kind = Glob_term.binding_kind [@@deriving sexp,yojson,hash,compare]
-type 'a glob_sort_gen = 'a Glob_term.glob_sort_gen [@@deriving sexp,yojson,hash,compare]
+type binding_kind = Glob_term.binding_kind [@@deriving sexp,yojson,python,hash,compare]
+type 'a glob_sort_gen = 'a Glob_term.glob_sort_gen [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_level = Glob_term.glob_level
 val glob_level_of_sexp : Sexp.t -> Glob_term.glob_level
@@ -31,19 +31,15 @@ val sexp_of_glob_sort : Glob_term.glob_sort -> Sexp.t
 val glob_sort_of_yojson : Yojson.Safe.t -> (glob_sort, string) Result.result
 val glob_sort_to_yojson : glob_sort -> Yojson.Safe.t
 
-(* type 'a cast_type = 'a Glob_term.cast_type
- * val cast_type_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a Glob_term.cast_type
- * val sexp_of_cast_type : ('a -> Sexp.t) -> 'a Glob_term.cast_type -> Sexp.t
- * val cast_type_of_yojson : (Yojson.Safe.t -> ('a,string) result ) -> Yojson.Safe.t -> ('a cast_type, string) Result.result
- * val cast_type_to_yojson : ('a -> Yojson.Safe.t) -> 'a cast_type -> Yojson.Safe.t *)
-
 type glob_constraint = Glob_term.glob_constraint
 val glob_constraint_of_sexp : Sexp.t -> Glob_term.glob_constraint
 val sexp_of_glob_constraint : Glob_term.glob_constraint -> Sexp.t
 val glob_constraint_of_yojson : Yojson.Safe.t -> (glob_constraint, string) Result.result
 val glob_constraint_to_yojson : glob_constraint -> Yojson.Safe.t
+val glob_constraint_of_python : Py.Object.t -> Glob_term.glob_constraint
+val python_of_glob_constraint : Glob_term.glob_constraint -> Py.Object.t
 
-type existential_name = Glob_term.existential_name [@@deriving sexp,yojson,hash,compare]
+type existential_name = Glob_term.existential_name [@@deriving sexp,yojson,python,hash,compare]
 type cases_pattern    = Glob_term.cases_pattern
 
 type glob_constr        = Glob_term.glob_constr
@@ -53,4 +49,4 @@ and tomatch_tuple       = Glob_term.tomatch_tuple
 and tomatch_tuples      = Glob_term.tomatch_tuples
 and cases_clause        = Glob_term.cases_clause
 and cases_clauses       = Glob_term.cases_clauses
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_globnames.ml b/serlib/ser_globnames.ml
index 598a9794..9392d36f 100644
--- a/serlib/ser_globnames.ml
+++ b/serlib/ser_globnames.ml
@@ -17,8 +17,8 @@ module Names = Ser_names
 
 type abbreviation =
   [%import: Globnames.abbreviation]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type extended_global_reference =
   [%import: Globnames.extended_global_reference]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/ser_goal_select.ml b/serlib/ser_goal_select.ml
index d42ecade..31165680 100644
--- a/serlib/ser_goal_select.ml
+++ b/serlib/ser_goal_select.ml
@@ -15,16 +15,13 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-(* type goal_selector = Vernacexpr.goal_selector
- * val goal_selector_of_sexp : Sexp.t -> goal_selector
- * val sexp_of_goal_selector : goal_selector -> Sexp.t *)
-
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
 
 module Names       = Ser_names
 
 type t =
   [%import: Goal_select.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_goptions.ml b/serlib/ser_goptions.ml
index 71b4a87f..b5ee9cc6 100644
--- a/serlib/ser_goptions.ml
+++ b/serlib/ser_goptions.ml
@@ -15,29 +15,30 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module Libnames = Ser_libnames
 
 type option_locality =
   [%import: Goptions.option_locality]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
 
 type option_name =
   [%import: Goptions.option_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type option_value =
   [%import: Goptions.option_value]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type option_state =
   [%import: Goptions.option_state]
-  [@@deriving sexp]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type table_value =
   [%import: Goptions.table_value]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
diff --git a/serlib/ser_goptions.mli b/serlib/ser_goptions.mli
index c22c2168..93fb28f9 100644
--- a/serlib/ser_goptions.mli
+++ b/serlib/ser_goptions.mli
@@ -22,18 +22,13 @@ type option_locality = Goptions.option_locality
 val option_locality_of_sexp : Sexp.t -> option_locality
 val sexp_of_option_locality : option_locality -> Sexp.t
 
-type option_name = Goptions.option_name [@@deriving sexp, yojson, hash,compare]
+type option_name = Goptions.option_name [@@deriving sexp,yojson,python,hash,compare]
 
 type option_value = Goptions.option_value
-
-val option_value_of_sexp : Sexp.t -> option_value
-val sexp_of_option_value : option_value -> Sexp.t
-val option_value_of_yojson : Yojson.Safe.t -> (option_value, string) Result.result
-val option_value_to_yojson : option_value -> Yojson.Safe.t
+[@@deriving sexp,yojson,python,hash,compare]
 
 type option_state = Goptions.option_state
+[@@deriving sexp,yojson,python,hash,compare]
 
-val option_state_of_sexp : Sexp.t -> option_state
-val sexp_of_option_state : option_state -> Sexp.t
-
-type table_value = Goptions.table_value [@@deriving sexp, yojson, hash,compare]
+type table_value = Goptions.table_value
+[@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_gramlib.ml b/serlib/ser_gramlib.ml
index 2068fb23..333a83a3 100644
--- a/serlib/ser_gramlib.ml
+++ b/serlib/ser_gramlib.ml
@@ -16,5 +16,5 @@
 module Gramext = struct
   type g_assoc =
     [%import: Gramlib.Gramext.g_assoc]
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 end
diff --git a/serlib/ser_hints.ml b/serlib/ser_hints.ml
index 96e2fff6..abd5fc57 100644
--- a/serlib/ser_hints.ml
+++ b/serlib/ser_hints.ml
@@ -13,9 +13,10 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
 
 module Names       = Ser_names
 module Libnames    = Ser_libnames
@@ -25,24 +26,24 @@ module Genarg      = Ser_genarg
 
 type hint_db_name =
   [%import: Hints.hint_db_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a hints_path_atom_gen =
   [%import: 'a Hints.hints_path_atom_gen]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a hints_path_gen =
   [%import: 'a Hints.hints_path_gen]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type hints_path =
   [%import: Hints.hints_path]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type hint_mode =
   [%import: Hints.hint_mode]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a hints_transparency_target =
   [%import: 'a Hints.hints_transparency_target]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_hints.mli b/serlib/ser_hints.mli
index ce89395f..5c79d545 100644
--- a/serlib/ser_hints.mli
+++ b/serlib/ser_hints.mli
@@ -14,16 +14,16 @@
 (************************************************************************)
 
 type hint_db_name = Hints.hint_db_name
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a hints_path_gen = 'a Hints.hints_path_gen
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a hints_path_atom_gen = 'a Hints.hints_path_atom_gen
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type hints_path = Hints.hints_path
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
-type 'a hints_transparency_target = 'a Hints.hints_transparency_target [@@deriving sexp,yojson,hash,compare]
-type hint_mode = Hints.hint_mode [@@deriving sexp,yojson,hash,compare]
+type 'a hints_transparency_target = 'a Hints.hints_transparency_target [@@deriving sexp,yojson,python,hash,compare]
+type hint_mode = Hints.hint_mode [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_impargs.ml b/serlib/ser_impargs.ml
index eb9af4b1..39fe5767 100644
--- a/serlib/ser_impargs.ml
+++ b/serlib/ser_impargs.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -22,30 +23,32 @@ module Constrexpr = Ser_constrexpr
 
 type argument_position =
   [%import: Impargs.argument_position]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type implicit_explanation =
   [%import: Impargs.implicit_explanation]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type maximal_insertion =
   [%import: Impargs.maximal_insertion]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type force_inference =
   [%import: Impargs.force_inference]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 module ISCPierceSpec = struct
   type t = Impargs.implicit_side_condition
   type _t = DefaultImpArgs | LessArgsThan of int
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module B_ = SerType.Pierce(ISCPierceSpec)
 type implicit_side_condition = B_.t
 let sexp_of_implicit_side_condition = B_.sexp_of_t
 let implicit_side_condition_of_sexp = B_.t_of_sexp
+let python_of_implicit_side_condition = B_.python_of_t
+let implicit_side_condition_of_python = B_.t_of_python
 let implicit_side_condition_of_yojson = B_.of_yojson
 let implicit_side_condition_to_yojson = B_.to_yojson
 let hash_implicit_side_condition = B_.hash
@@ -54,16 +57,12 @@ let compare_implicit_side_condition = B_.compare
 
 type implicit_position =
   [%import: Impargs.implicit_position]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type implicit_status =
   [%import: Impargs.implicit_status]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type implicits_list =
   [%import: Impargs.implicits_list]
-  [@@deriving sexp]
-
-
-
-
+  [@@deriving sexp,python]
diff --git a/serlib/ser_impargs.mli b/serlib/ser_impargs.mli
index 4e9b7fea..cc99d701 100644
--- a/serlib/ser_impargs.mli
+++ b/serlib/ser_impargs.mli
@@ -47,3 +47,6 @@ type implicits_list = Impargs.implicits_list
 
 val implicits_list_of_sexp : Sexp.t -> implicits_list
 val sexp_of_implicits_list : implicits_list -> Sexp.t
+
+val implicits_list_of_python : Py.Object.t -> implicits_list
+val python_of_implicits_list : implicits_list -> Py.Object.t
diff --git a/serlib/ser_int.ml b/serlib/ser_int.ml
index 6253eac8..a3a9bae3 100644
--- a/serlib/ser_int.ml
+++ b/serlib/ser_int.ml
@@ -14,11 +14,12 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
 
 type t =
   [%import: Int.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
diff --git a/serlib/ser_int.mli b/serlib/ser_int.mli
index d3b220fc..080ad15a 100644
--- a/serlib/ser_int.mli
+++ b/serlib/ser_int.mli
@@ -15,4 +15,4 @@
 (************************************************************************)
 
 type t = Int.t
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_lib.ml b/serlib/ser_lib.ml
index 152dc526..79750fb5 100644
--- a/serlib/ser_lib.ml
+++ b/serlib/ser_lib.ml
@@ -13,6 +13,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 module Nametab = Ser_nametab
 module Libobject = Ser_libobject
@@ -20,20 +21,20 @@ module Summary = Ser_summary
 
 type is_type =
   [%import: Lib.is_type]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type export_flag =
   [%import: Lib.export_flag]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type export =
   [%import: Lib.export]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type node =
   [%import: Lib.node]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type library_segment =
   [%import: Lib.library_segment]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/ser_libnames.ml b/serlib/ser_libnames.ml
index bfac3b74..29e01c1e 100644
--- a/serlib/ser_libnames.ml
+++ b/serlib/ser_libnames.ml
@@ -15,60 +15,64 @@
 
 (* open Sexplib.Std *)
 
+include Ppx_python_runtime
+
 let cmake = CAst.make
 
 module Loc   = Ser_loc
 module CAst  = Ser_cAst
 module Names = Ser_names
 
-type _t =
-  | Ser_Qualid of Names.DirPath.t * Names.Id.t
-    [@@deriving sexp,yojson,hash,compare]
-
-let _t_put qid =
-  let (dp, id) = Libnames.repr_qualid (cmake qid) in
-  Ser_Qualid (dp, id)
-
-let _t_get (Ser_Qualid (dp, id)) = Libnames.(make_qualid dp id).CAst.v
-
-type qualid_r =
-  [%import: Libnames.qualid_r]
+module QIDBIJ = struct
+  type t = Libnames.qualid_r
+  type _t =
+    | Ser_Qualid of Names.DirPath.t * Names.Id.t
+    [@@deriving sexp,yojson,python,hash,compare]
 
-let qualid_r_of_sexp sexp = _t_get (_t_of_sexp sexp)
-let sexp_of_qualid_r qid  = sexp_of__t (_t_put qid)
+  let of_t qid =
+    let (dp, id) = Libnames.repr_qualid (cmake qid) in
+    Ser_Qualid (dp, id)
+  let to_t (Ser_Qualid (dp, id)) = Libnames.(make_qualid dp id).CAst.v
+end
 
-let qualid_r_of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get)
-let qualid_r_to_yojson level = _t_to_yojson (_t_put level)
+module QID = SerType.Biject(QIDBIJ)
 
-(* let hash_qualid_r x = hash__t (_t_put x) *)
-let hash_fold_qualid_r st x = hash_fold__t st (_t_put x)
-let compare_qualid_r x y = compare__t (_t_put x) (_t_put y)
+type qualid_r = QID.t
+let sexp_of_qualid_r = QID.sexp_of_t
+let qualid_r_of_sexp = QID.t_of_sexp
+let python_of_qualid_r = QID.python_of_t
+let qualid_r_of_python = QID.t_of_python
+let qualid_r_of_yojson = QID.of_yojson
+let qualid_r_to_yojson = QID.to_yojson
+(* let hash_qualid_r = QID.hash *)
+let hash_fold_qualid_r = QID.hash_fold_t
+let compare_qualid_r = QID.compare
 
 (* qualid: private *)
 type qualid =
   [%import: Libnames.qualid]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module FP = struct
+  type t = Libnames.full_path
   type _t =
     { dirpath : Names.DirPath.t
     ; basename : Names.Id.t }
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
-  let _t_get { dirpath; basename } = Libnames.make_path dirpath basename
-  let _t_put fp = let dirpath, basename = Libnames.repr_path fp in { dirpath; basename }
+  let to_t { dirpath; basename } = Libnames.make_path dirpath basename
+  let of_t fp = let dirpath, basename = Libnames.repr_path fp in { dirpath; basename }
 end
 
-open FP
-
-type full_path = Libnames.full_path
-let full_path_of_sexp sexp = _t_get (_t_of_sexp sexp)
-let sexp_of_full_path qid  = sexp_of__t (_t_put qid)
-
-let full_path_of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get)
-let full_path_to_yojson level = _t_to_yojson (_t_put level)
-
-let hash_full_path x = hash__t (_t_put x)
-let hash_fold_full_path st x = hash_fold__t st (_t_put x)
-
-let compare_full_path x y = compare__t (_t_put x) (_t_put y)
+module F = SerType.Biject(FP)
+
+type full_path = F.t
+let sexp_of_full_path = F.sexp_of_t
+let full_path_of_sexp = F.t_of_sexp
+let python_of_full_path = F.python_of_t
+let full_path_of_python = F.t_of_python
+let full_path_of_yojson = F.of_yojson
+let full_path_to_yojson = F.to_yojson
+let hash_full_path = F.hash
+let hash_fold_full_path = F.hash_fold_t
+let compare_full_path = F.compare
diff --git a/serlib/ser_libnames.mli b/serlib/ser_libnames.mli
index df2e429a..09e37a6a 100644
--- a/serlib/ser_libnames.mli
+++ b/serlib/ser_libnames.mli
@@ -13,5 +13,5 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-type qualid = Libnames.qualid [@@deriving sexp,yojson,hash,compare]
-type full_path = Libnames.full_path [@@deriving sexp,yojson,hash,compare]
+type qualid = Libnames.qualid [@@deriving sexp,yojson,python,hash,compare]
+type full_path = Libnames.full_path [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_libobject.ml b/serlib/ser_libobject.ml
index 82319aae..d7bceca5 100644
--- a/serlib/ser_libobject.ml
+++ b/serlib/ser_libobject.ml
@@ -13,29 +13,30 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 module Names = Ser_names
 module Mod_subst = Ser_mod_subst
 
 module CString = struct
-  module Pred = struct
-    include CString.Pred
-    let t_of_sexp _ = CString.Pred.empty
-    let sexp_of_t _ = Sexplib.Sexp.Atom "XXX: CString.Pred.t"
-  end
+  module OP = struct type t = CString.Pred.t let name = "CString.Pred.t" end
+  module Pred = SerType.Opaque(OP)
 end
 
-type _open_filter =
-  | Unfiltered
-  | Filtered of CString.Pred.t
-  [@@deriving sexp]
-
-let _t_put x = Obj.magic x
-let _t_get x = Obj.magic x
+module OPP = struct
+  type t = Libobject.open_filter
+  type _t =
+    | Unfiltered
+    | Filtered of CString.Pred.t
+  [@@deriving sexp,yojson,python,hash,compare]
+end
 
-type open_filter = [%import: Libobject.open_filter]
-let open_filter_of_sexp x = _t_put (_open_filter_of_sexp x)
-let sexp_of_open_filter x = sexp_of__open_filter (_t_get x)
+module OF = SerType.Pierce(OPP)
+type open_filter = OF.t
+let open_filter_of_sexp = OF.t_of_sexp
+let sexp_of_open_filter = OF.sexp_of_t
+let open_filter_of_python = OF.t_of_python
+let python_of_open_filter = OF.python_of_t
 
 module Dyn = struct
 
@@ -47,7 +48,7 @@ module Dyn = struct
       (* | Constant of Internal.Constant.t
        * | Inductive of DeclareInd.Internal.inductive_obj *)
       | TaggedAnon of string
-    [@@deriving sexp]
+    [@@deriving sexp,python]
 
     let to_t (x : Libobject.Dyn.t) =
       let Libobject.Dyn.Dyn (tag, _) = x in
@@ -56,14 +57,16 @@ module Dyn = struct
 
   let t_of_sexp x = Serlib_base.opaque_of_sexp ~typ:"Libobject.Dyn.t" x
   let sexp_of_t x = Reified.sexp_of_t (Reified.to_t x)
+  let t_of_python x = Serlib_base.opaque_of_python ~typ:"Libobject.Dyn.t" x
+  let python_of_t x = Reified.python_of_t (Reified.to_t x)
 end
 
 type obj =
   [%import: Libobject.obj]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type algebraic_objects =
   [%import: Libobject.algebraic_objects]
 and t = [%import: Libobject.t]
 and substitutive_objects = [%import: Libobject.substitutive_objects]
-[@@deriving sexp]
+[@@deriving sexp,python]
diff --git a/serlib/ser_loadpath.ml b/serlib/ser_loadpath.ml
index d2689e42..eb3cc5d8 100644
--- a/serlib/ser_loadpath.ml
+++ b/serlib/ser_loadpath.ml
@@ -16,12 +16,14 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
+
 module Names = Ser_names
 
 type library_location =
   [%import: Loadpath.library_location]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type vo_path =
   [%import: Loadpath.vo_path]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/ser_loc.ml b/serlib/ser_loc.ml
index e0e1abb9..9a492056 100644
--- a/serlib/ser_loc.ml
+++ b/serlib/ser_loc.ml
@@ -18,16 +18,17 @@
 (**********************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
 type source =
   [%import: Loc.source]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type t =
   [%import: Loc.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let omit_loc = ref false
 let sexp_of_t x =
@@ -35,4 +36,4 @@ let sexp_of_t x =
 
 (* located: public *)
 type 'a located = (t option [@ignore]) * 'a
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_loc.mli b/serlib/ser_loc.mli
index 818dcd92..783512ad 100644
--- a/serlib/ser_loc.mli
+++ b/serlib/ser_loc.mli
@@ -18,10 +18,10 @@
 (**********************************************************************)
 
 type t = Loc.t
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* Don't print locations. Global-flag Hack. *)
 val omit_loc : bool ref
 
 type 'a located = 'a Loc.located
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_locus.ml b/serlib/ser_locus.ml
index 16721d18..e3f8155c 100644
--- a/serlib/ser_locus.ml
+++ b/serlib/ser_locus.ml
@@ -13,27 +13,28 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module Names     = Ser_names
 
 type 'a or_var =
   [%import: 'a Locus.or_var]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a occurrences_gen =
   [%import: 'a Locus.occurrences_gen]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type occurrences_expr =
   [%import: Locus.occurrences_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a with_occurrences =
   [%import: 'a Locus.with_occurrences]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type occurrences =
   [%import: Locus.occurrences]
@@ -41,15 +42,15 @@ type occurrences =
 
 type hyp_location_flag =
   [%import: Locus.hyp_location_flag]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a hyp_location_expr =
   [%import: 'a Locus.hyp_location_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'id clause_expr =
   [%import: 'id Locus.clause_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type clause =
   [%import: Locus.clause]
@@ -65,7 +66,7 @@ type concrete_clause =
 
 type hyp_location =
   [%import: Locus.hyp_location]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type goal_location =
   [%import: Locus.goal_location]
diff --git a/serlib/ser_locus.mli b/serlib/ser_locus.mli
index 989598f0..f0c40a89 100644
--- a/serlib/ser_locus.mli
+++ b/serlib/ser_locus.mli
@@ -16,7 +16,7 @@
 open Sexplib
 
 type 'a or_var = 'a Locus.or_var
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a occurrences_gen = 'a Locus.occurrences_gen
 val occurrences_gen_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a occurrences_gen
@@ -27,7 +27,7 @@ type occurrences_expr = Locus.occurrences_expr
 val occurrences_expr_of_sexp : Sexp.t -> occurrences_expr
 val sexp_of_occurrences_expr : occurrences_expr -> Sexp.t
 
-type 'a with_occurrences = 'a Locus.with_occurrences [@@deriving sexp, yojson, hash,compare]
+type 'a with_occurrences = 'a Locus.with_occurrences [@@deriving sexp,yojson,python,hash,compare]
 
 type occurrences = Locus.occurrences
 val occurrences_of_sexp : Sexp.t -> occurrences
@@ -41,7 +41,7 @@ val hyp_location_expr_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a hyp_location_expr
 val sexp_of_hyp_location_expr : ('a -> Sexp.t) -> 'a hyp_location_expr -> Sexp.t
 
 type 'id clause_expr = 'id Locus.clause_expr
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type clause = Locus.clause
 
@@ -59,7 +59,7 @@ val concrete_clause_of_sexp : Sexp.t -> concrete_clause
 val sexp_of_concrete_clause : concrete_clause -> Sexp.t
 
 type hyp_location = Locus.hyp_location
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type goal_location = Locus.goal_location
 
diff --git a/serlib/ser_mod_subst.ml b/serlib/ser_mod_subst.ml
index 2184f5e2..d85761c1 100644
--- a/serlib/ser_mod_subst.ml
+++ b/serlib/ser_mod_subst.ml
@@ -27,6 +27,8 @@ module A_ = SerType.Opaque(OD)
 type delta_resolver = A_.t
 let sexp_of_delta_resolver = A_.sexp_of_t
 let delta_resolver_of_sexp = A_.t_of_sexp
+let python_of_delta_resolver = A_.python_of_t
+let delta_resolver_of_python = A_.t_of_python
 let delta_resolver_of_yojson = A_.of_yojson
 let delta_resolver_to_yojson = A_.to_yojson
 let hash_delta_resolver = A_.hash
@@ -43,6 +45,8 @@ module B_ = SerType.Opaque(OS)
 type substitution = B_.t
 let sexp_of_substitution = B_.sexp_of_t
 let substitution_of_sexp = B_.t_of_sexp
+let python_of_substitution = B_.python_of_t
+let substitution_of_python = B_.t_of_python
 let substitution_of_yojson = B_.of_yojson
 let substitution_to_yojson = B_.to_yojson
 let hash_substitution = B_.hash
diff --git a/serlib/ser_mod_subst.mli b/serlib/ser_mod_subst.mli
index 3770dede..26236998 100644
--- a/serlib/ser_mod_subst.mli
+++ b/serlib/ser_mod_subst.mli
@@ -14,11 +14,7 @@
 (************************************************************************)
 
 type delta_resolver = Mod_subst.delta_resolver
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type substitution = Mod_subst.substitution
- [@@deriving sexp,yojson,hash,compare]
-
-(* type 'a substituted = 'a Mod_subst.substituted
- * val sexp_of_substituted : ('a -> Sexp.t) -> 'a substituted -> Sexp.t
- * val substituted_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a substituted *)
+ [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_namegen.ml b/serlib/ser_namegen.ml
index e25cfeec..201f3468 100644
--- a/serlib/ser_namegen.ml
+++ b/serlib/ser_namegen.ml
@@ -19,4 +19,4 @@ module Names      = Ser_names
 
 type intro_pattern_naming_expr =
   [%import: Namegen.intro_pattern_naming_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_names.ml b/serlib/ser_names.ml
index 4f37b1aa..72527103 100644
--- a/serlib/ser_names.ml
+++ b/serlib/ser_names.ml
@@ -17,6 +17,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -34,13 +35,12 @@ module Id = struct
   (* Id.t: private *)
   module Id_ = struct
     type t = Names.Id.t
-    type _t = Id of string [@@deriving sexp, yojson, hash, compare]
+    type _t = Id of string [@@deriving sexp,yojson,python,hash,compare]
     let of_t id = Id (Id.to_string id)
     let to_t (Id id) = Id.of_string_soft id
   end
 
   module Self = SerType.Biject(Id_)
-
   include Self
 
   module Set = Ser_cSet.Make(Names.Id.Set)(Self)
@@ -53,7 +53,7 @@ module Name = struct
 (* Name.t: public *)
 type t =
   [%import: Names.Name.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 end
 
@@ -63,7 +63,7 @@ module DirPath = struct
   module DirPath_ = struct
     type t = Names.DirPath.t
     type _t = DirPath of Id.t list
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
     let of_t dp = DirPath (DirPath.repr dp)
     let to_t (DirPath dpl) = DirPath.make dpl
@@ -83,7 +83,7 @@ module Label = struct
 
     (* XXX: This will miss the tag *)
     type _t = Id.t
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
     let to_t = Label.of_id
     let of_t = Label.to_id
@@ -99,7 +99,7 @@ module MBId = struct
     type t = [%import: Names.MBId.t]
 
     type _t = Mbid of int * Id.t * DirPath.t
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
   end
 
@@ -111,8 +111,7 @@ module ModPath = struct
 
 (* ModPath.t: public *)
 type t = [%import: Names.ModPath.t]
-         [@@deriving sexp,yojson,hash,compare]
-
+         [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module MPmap = Ser_cMap.Make(MPmap)(ModPath)
@@ -120,55 +119,37 @@ module MPmap = Ser_cMap.Make(MPmap)(ModPath)
 (* KerName: private *)
 module KerName = struct
 
-type t = [%import: Names.KerName.t]
-
-type _t = KerName of ModPath.t * Label.t
-      [@@deriving sexp,yojson,hash,compare]
-
-let _t_put kn              =
-  let mp, l = KerName.repr kn in KerName (mp,l)
-let _kername_get (KerName (mp,l)) = KerName.make mp l
-
-let t_of_sexp sexp = _kername_get (_t_of_sexp sexp)
-let sexp_of_t kn   = sexp_of__t (_t_put kn)
+  module KerBij = struct
+    type t = Names.KerName.t
+    type _t = KerName of ModPath.t * Label.t
+    [@@deriving sexp,yojson,python,hash,compare]
 
-let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _kername_get)
-let to_yojson kn   = _t_to_yojson (_t_put kn)
-
-let hash x = hash__t (_t_put x)
-let hash_fold_t st id = hash_fold__t st (_t_put id)
-
-let compare x y = compare__t (_t_put x) (_t_put y)
+    let of_t kn = let mp, l = KerName.repr kn in KerName (mp,l)
+    let to_t (KerName (mp,l)) = KerName.make mp l
+  end
 
-let equal = KerName.equal
+  let equal = KerName.equal
+  include SerType.Biject(KerBij)
 
 end
 
 module Constant = struct
 
-(* Constant.t: private *)
-type t = [%import: Names.Constant.t]
-
-type _t = Constant of KerName.t * KerName.t option
-      [@@deriving sexp,yojson,hash,compare]
+  module ConBij = struct
+    (* Constant.t: private *)
+    type t = Names.Constant.t
+    type _t = Constant of KerName.t * KerName.t option
+    [@@deriving sexp,yojson,python,hash,compare]
 
-let _t_put cs =
-  let cu, cc = Constant.(user cs, canonical cs) in
-  if KerName.equal cu cc then Constant (cu, None) else Constant (cu, Some cc)
-let _t_get = function
-  | Constant (cu, None) -> Constant.make1 cu
-  | Constant (cu, Some cc) -> Constant.make cu cc
-
-let t_of_sexp sexp = _t_get (_t_of_sexp sexp)
-let sexp_of_t dp   = sexp_of__t (_t_put dp)
-
-let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get)
-let to_yojson level = _t_to_yojson (_t_put level)
-
-let hash x = hash__t (_t_put x)
-let hash_fold_t st id = hash_fold__t st (_t_put id)
+    let of_t cs =
+      let cu, cc = Constant.(user cs, canonical cs) in
+      if KerName.equal cu cc then Constant (cu, None) else Constant (cu, Some cc)
+    let to_t = function
+      | Constant (cu, None) -> Constant.make1 cu
+      | Constant (cu, Some cc) -> Constant.make cu cc
+  end
 
-let compare x y = compare__t (_t_put x) (_t_put y)
+  include SerType.Biject(ConBij)
 
 end
 
@@ -183,7 +164,7 @@ module MutInd = struct
   module BijectSpec = struct
     type t = [%import: Names.MutInd.t]
     type _t = MutInd of KerName.t * KerName.t option
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
     let of_t cs =
       let cu, cc = MutInd.(user cs, canonical cs) in
@@ -206,30 +187,30 @@ type 'a tableKey =
 
 type variable =
   [%import: Names.variable]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* Inductive and constructor = public *)
 module Ind = struct
   type t =
   [%import: Names.Ind.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module Indset_env = Ser_cSet.Make(Indset_env)(Ind)
 
 type inductive =
   [%import: Names.inductive]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module Construct = struct
   type t =
   [%import: Names.Construct.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 end
 type constructor =
   [%import: Names.constructor]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* Projection: private *)
 module Projection = struct
@@ -243,7 +224,7 @@ module Projection = struct
         ; proj_npars : int
         ; proj_arg : int
         ; proj_name : Label.t
-        } [@@deriving sexp,yojson,hash,compare]
+        } [@@deriving sexp,yojson,python,hash,compare]
     end
     include SerType.Pierce(PierceSpec)
   end
@@ -251,31 +232,24 @@ module Projection = struct
   module PierceSpec = struct
     type t = [%import: Names.Projection.t]
     type _t = Repr.t * bool
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
   end
   include SerType.Pierce(PierceSpec)
 end
 
 module GlobRef = struct
-
-type t = [%import: Names.GlobRef.t]
-  [@@deriving sexp,yojson,hash,compare]
-
+  type t = [%import: Names.GlobRef.t]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
-(* Evaluable global reference: public *)
-(* type evaluable_global_reference =
- *   [%import: Names.evaluable_global_reference]
- *   [@@deriving sexp] *)
-
 type lident =
   [%import: Names.lident]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type lname =
   [%import: Names.lname]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type lstring =
   [%import: Names.lstring]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_names.mli b/serlib/ser_names.mli
index e920e3c9..bcc27933 100644
--- a/serlib/ser_names.mli
+++ b/serlib/ser_names.mli
@@ -20,30 +20,30 @@ open Names
 open Sexplib
 
 module Id : sig
-  include SerType.SJHC with type t = Id.t
+  include SerType.SJPHC with type t = Id.t
 
-  module Set : SerType.SJHC with type t = Id.Set.t
-  module Map : SerType.SJHC1 with type 'a t = 'a Id.Map.t
+  module Set : SerType.SJPHC with type t = Id.Set.t
+  module Map : SerType.SJPHC1 with type 'a t = 'a Id.Map.t
 end
 
-module Name    : SerType.SJHC with type t = Name.t
-module DirPath : SerType.SJHC with type t = DirPath.t
+module Name    : SerType.SJPHC with type t = Name.t
+module DirPath : SerType.SJPHC with type t = DirPath.t
 module DPmap   : Ser_cMap.ExtS with type key = DirPath.t and type 'a t = 'a DPmap.t
 
-module Label   : SerType.SJHC with type t = Label.t
-module MBId    : SerType.SJHC with type t = MBId.t
-module ModPath : SerType.SJHC with type t = ModPath.t
+module Label   : SerType.SJPHC with type t = Label.t
+module MBId    : SerType.SJPHC with type t = MBId.t
+module ModPath : SerType.SJPHC with type t = ModPath.t
 module MPmap   : Ser_cMap.ExtS with type key = ModPath.t and type 'a t = 'a MPmap.t
 
-module KerName  : SerType.SJHC with type t = KerName.t
-module Constant : SerType.SJHC with type t = Constant.t
+module KerName  : SerType.SJPHC with type t = KerName.t
+module Constant : SerType.SJPHC with type t = Constant.t
 
 module Cset_env : Ser_cSet.ExtS with type elt = Constant.t and type t = Cset_env.t
 
 module Cmap : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Cmap.t
 module Cmap_env : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Cmap_env.t
 
-module MutInd : SerType.S with type t = MutInd.t
+module MutInd : SerType.SJP with type t = MutInd.t
 
 module Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindmap.t
 module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindmap_env.t
@@ -55,13 +55,15 @@ type 'a tableKey = 'a Names.tableKey
 val tableKey_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a tableKey
 val sexp_of_tableKey : ('a -> Sexp.t) -> 'a tableKey -> Sexp.t
 
-type variable    = Names.variable [@@deriving sexp, yojson, hash, compare]
-type inductive   = Names.inductive [@@deriving sexp, yojson, hash, compare]
-type constructor = Names.constructor [@@deriving sexp, yojson, hash, compare]
+type variable    = Names.variable [@@deriving sexp,yojson,python,hash,compare]
+type inductive   = Names.inductive [@@deriving sexp,yojson,python,hash,compare]
+type constructor = Names.constructor [@@deriving sexp,yojson,python,hash,compare]
+
+(* -- end modularize -- *)
 
 module Projection : sig
 
-  include SerType.SJHC with type t = Projection.t
+  include SerType.SJPHC with type t = Projection.t
 
   module Repr : sig
     include SerType.S with type t = Projection.Repr.t
@@ -69,8 +71,8 @@ module Projection : sig
 
 end
 
-module GlobRef : SerType.SJHC with type t = Names.GlobRef.t
+module GlobRef : SerType.SJPHC with type t = Names.GlobRef.t
 
-type lident = Names.lident [@@deriving sexp,yojson,hash,compare]
-type lname = Names.lname [@@deriving sexp,yojson,hash,compare]
-type lstring = Names.lstring [@@deriving sexp,yojson,hash,compare]
+type lident = Names.lident [@@deriving sexp,yojson,python,hash,compare]
+type lname = Names.lname [@@deriving sexp,yojson,python,hash,compare]
+type lstring = Names.lstring [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_nametab.ml b/serlib/ser_nametab.ml
index 760aa306..893e67c0 100644
--- a/serlib/ser_nametab.ml
+++ b/serlib/ser_nametab.ml
@@ -13,8 +13,10 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Ppx_python_runtime
+
 module Names = Ser_names
 
 type object_prefix =
   [%import: Nametab.object_prefix]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/ser_nametab.mli b/serlib/ser_nametab.mli
index 8b6aab62..a65b5c0e 100644
--- a/serlib/ser_nametab.mli
+++ b/serlib/ser_nametab.mli
@@ -13,5 +13,4 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-type object_prefix = Nametab.object_prefix [@@deriving sexp]
-
+type object_prefix = Nametab.object_prefix [@@deriving sexp,python]
diff --git a/serlib/ser_nativevalues.ml b/serlib/ser_nativevalues.ml
index 780709ee..97327e44 100644
--- a/serlib/ser_nativevalues.ml
+++ b/serlib/ser_nativevalues.ml
@@ -16,6 +16,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 module Names  = Ser_names
 module Evar   = Ser_evar
@@ -29,15 +30,15 @@ type t =
 
 type tag =
   [%import: Nativevalues.tag]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type arity =
   [%import: Nativevalues.arity]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type reloc_table =
   [%import: Nativevalues.reloc_table]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type annot_sw =
   [%import: Nativevalues.annot_sw]
diff --git a/serlib/ser_notation.ml b/serlib/ser_notation.ml
index 7b0885e5..8fde2faf 100644
--- a/serlib/ser_notation.ml
+++ b/serlib/ser_notation.ml
@@ -14,14 +14,12 @@
 (************************************************************************)
 
 open Sexplib.Std
-
-(* module Ppextend = Ser_ppextend
- * module Notation_term = Ser_notation_term *)
+open Ppx_python_runtime
 
 module Constrexpr = Ser_constrexpr
 
 type level =
   [%import: Notation.level]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
 
 
diff --git a/serlib/ser_notation.mli b/serlib/ser_notation.mli
index df562d86..cfd5a87f 100644
--- a/serlib/ser_notation.mli
+++ b/serlib/ser_notation.mli
@@ -18,3 +18,5 @@ open Sexplib
 type level = Notation.level
 val level_of_sexp : Sexp.t -> level
 val sexp_of_level : level -> Sexp.t
+val level_of_python : Py.Object.t -> level
+val python_of_level : level -> Py.Object.t
diff --git a/serlib/ser_notation_gram.ml b/serlib/ser_notation_gram.ml
index 9c51d661..0aa07ce8 100644
--- a/serlib/ser_notation_gram.ml
+++ b/serlib/ser_notation_gram.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Conv
+open Ppx_python_runtime
 
 module Names         = Ser_names
 module Constrexpr    = Ser_constrexpr
@@ -22,26 +23,14 @@ module Extend        = Ser_extend
 module Gramlib       = Ser_gramlib
 module Notation      = Ser_notation
 
-(* type precedence =
- *   [%import: Notation_gram.precedence]
- *   [@@deriving sexp] *)
-
-(* type parenRelation =
- *   [%import: Notation_gram.parenRelation]
- *   [@@deriving sexp] *)
-
-(* type tolerability =
- *   [%import: Notation_gram.tolerability]
- *   [@@deriving sexp] *)
-
 type grammar_constr_prod_item =
   [%import: Notation_gram.grammar_constr_prod_item]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type one_notation_grammar =
   [%import: Notation_gram.one_notation_grammar]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type notation_grammar =
   [%import: Notation_gram.notation_grammar]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/ser_notation_gram.mli b/serlib/ser_notation_gram.mli
index a08ad5ab..3cd70822 100644
--- a/serlib/ser_notation_gram.mli
+++ b/serlib/ser_notation_gram.mli
@@ -15,21 +15,6 @@
 
 open Sexplib
 
-(* type parenRelation = Notation_gram.parenRelation
- * 
- * val parenRelation_of_sexp : Sexp.t -> parenRelation
- * val sexp_of_parenRelation : parenRelation -> Sexp.t
- * 
- * type precedence = Notation_gram.precedence
- * 
- * val precedence_of_sexp : Sexp.t -> precedence
- * val sexp_of_precedence : precedence -> Sexp.t
- * 
- * type tolerability = Notation_gram.tolerability
- * 
- * val tolerability_of_sexp : Sexp.t -> tolerability
- * val sexp_of_tolerability : tolerability -> Sexp.t *)
-
 type grammar_constr_prod_item = Notation_gram.grammar_constr_prod_item
 val grammar_constr_prod_item_of_sexp : Sexp.t -> grammar_constr_prod_item
 val sexp_of_grammar_constr_prod_item : grammar_constr_prod_item -> Sexp.t
@@ -37,4 +22,6 @@ val sexp_of_grammar_constr_prod_item : grammar_constr_prod_item -> Sexp.t
 type notation_grammar = Notation_gram.notation_grammar
 val notation_grammar_of_sexp : Sexp.t -> notation_grammar
 val sexp_of_notation_grammar : notation_grammar -> Sexp.t
+val notation_grammar_of_python : Py.Object.t -> notation_grammar
+val python_of_notation_grammar : notation_grammar -> Py.Object.t
 
diff --git a/serlib/ser_notation_term.ml b/serlib/ser_notation_term.ml
index ab9d23ab..b3a75f73 100644
--- a/serlib/ser_notation_term.ml
+++ b/serlib/ser_notation_term.ml
@@ -20,34 +20,27 @@ module Names      = Ser_names
 module Tok        = Ser_tok
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
 type scope_name =
   [%import: Notation_term.scope_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type tmp_scope_name =
   [%import: Notation_term.tmp_scope_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type subscopes =
   [%import: Notation_term.subscopes]
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type notation_spec = *)
-(*   [%import: Notation_term.notation_spec] *)
-(*   [@@deriving sexp] *)
-
-(* type syntax_modifier = *)
-(*   [%import: Notation_term.syntax_modifier] *)
-(*   [@@deriving sexp] *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constr_as_binder_kind =
   [%import: Notation_term.constr_as_binder_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type notation_var_internalization_type =
   [%import: Notation_term.notation_var_internalization_type]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
diff --git a/serlib/ser_notation_term.mli b/serlib/ser_notation_term.mli
index 44d27399..cc361136 100644
--- a/serlib/ser_notation_term.mli
+++ b/serlib/ser_notation_term.mli
@@ -14,10 +14,10 @@
 (************************************************************************)
 
 type subscopes = Notation_term.subscopes
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constr_as_binder_kind = Notation_term.constr_as_binder_kind
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type notation_var_internalization_type = Notation_term.notation_var_internalization_type
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_numTok.ml b/serlib/ser_numTok.ml
index 850527fa..f2d1fb9f 100644
--- a/serlib/ser_numTok.ml
+++ b/serlib/ser_numTok.ml
@@ -13,21 +13,22 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 type sign =
   [%import: NumTok.sign]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type num_class =
   [%import: NumTok.num_class]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
 
 type 'a exp =
   [%import: 'a NumTok.exp]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
 
 module Unsigned = struct
 
@@ -37,7 +38,7 @@ module Unsigned = struct
       int : string;
       frac : string;
       exp : string
-    } [@@deriving sexp,yojson,hash,compare]
+    } [@@deriving sexp,yojson,python,hash,compare]
   end
 
   include SerType.Pierce(PierceSpec)
@@ -47,6 +48,6 @@ module Signed = struct
 
   type t =
     [%import: NumTok.Signed.t]
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 
 end
diff --git a/serlib/ser_opaqueproof.ml b/serlib/ser_opaqueproof.ml
index 4affbd59..f8203499 100644
--- a/serlib/ser_opaqueproof.ml
+++ b/serlib/ser_opaqueproof.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_compare_lib.Builtin
 open Ppx_hash_lib.Std.Hash.Builtin
 
@@ -28,7 +29,7 @@ module OP = struct
 type t = [%import: Opaqueproof.opaque]
 type _t =
   | Indirect of Mod_subst.substitution list * Cooking.cooking_info list * Names.DirPath.t * int (* subst, discharge, lib, index *)
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module B_ = SerType.Pierce(OP)
@@ -36,6 +37,8 @@ module B_ = SerType.Pierce(OP)
 type opaque = Opaqueproof.opaque
 let sexp_of_opaque = B_.sexp_of_t
 let opaque_of_sexp = B_.t_of_sexp
+let python_of_opaque = B_.python_of_t
+let opaque_of_python = B_.t_of_python
 let opaque_of_yojson = B_.of_yojson
 let opaque_to_yojson = B_.to_yojson
 let hash_opaque = B_.hash
@@ -49,7 +52,7 @@ module OTSpec = struct
   type _t = {
     opaque_len : int;
     opaque_dir : Names.DirPath.t;
-  } [@@deriving sexp,yojson,hash,compare]
+  } [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module C_ = SerType.Pierce(OTSpec)
@@ -57,6 +60,8 @@ module C_ = SerType.Pierce(OTSpec)
 type opaquetab = C_.t
 let sexp_of_opaquetab = C_.sexp_of_t
 let opaquetab_of_sexp = C_.t_of_sexp
+let python_of_opaquetab = C_.python_of_t
+let opaquetab_of_python = C_.t_of_python
 let opaquetab_of_yojson = C_.of_yojson
 let opaquetab_to_yojson = C_.to_yojson
 let hash_opaquetab = C_.hash
diff --git a/serlib/ser_opaqueproof.mli b/serlib/ser_opaqueproof.mli
index aed56962..72f62957 100644
--- a/serlib/ser_opaqueproof.mli
+++ b/serlib/ser_opaqueproof.mli
@@ -14,7 +14,7 @@
 (************************************************************************)
 
 type opaque = Opaqueproof.opaque
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type opaquetab = Opaqueproof.opaquetab
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_pattern.ml b/serlib/ser_pattern.ml
index adbb6cdc..cf8ad233 100644
--- a/serlib/ser_pattern.ml
+++ b/serlib/ser_pattern.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -28,14 +29,14 @@ module Glob_term = Ser_glob_term
 
 type patvar =
   [%import: Pattern.patvar]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type case_info_pattern =
   [%import: Pattern.case_info_pattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let hash_fold_array = hash_fold_array_frozen
 
 type constr_pattern =
   [%import: Pattern.constr_pattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_pattern.mli b/serlib/ser_pattern.mli
index 126e7203..50745091 100644
--- a/serlib/ser_pattern.mli
+++ b/serlib/ser_pattern.mli
@@ -15,7 +15,7 @@
 
 open Sexplib
 
-type patvar = Pattern.patvar [@@deriving sexp,yojson,hash,compare]
+type patvar = Pattern.patvar [@@deriving sexp,yojson,python,hash,compare]
 
 type case_info_pattern = Pattern.case_info_pattern
 
@@ -23,4 +23,4 @@ val case_info_pattern_of_sexp : Sexp.t -> case_info_pattern
 val sexp_of_case_info_pattern : case_info_pattern -> Sexp.t
 
 type constr_pattern = Pattern.constr_pattern
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_pp.ml b/serlib/ser_pp.ml
index 9078a176..7e612af0 100644
--- a/serlib/ser_pp.ml
+++ b/serlib/ser_pp.ml
@@ -14,14 +14,15 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 type pp_tag =
   [%import: Pp.pp_tag]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp, yojson, python]
 
 type block_type =
   [%import: Pp.block_type]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp, yojson, python]
 
 module P = struct
   type _t =
@@ -34,7 +35,7 @@ module P = struct
   | Pp_print_break of int * int
   | Pp_force_newline
   | Pp_comment of string list
-  [@@deriving sexp, yojson]
+  [@@deriving sexp, yojson, python]
 
   open Pp
 
@@ -67,6 +68,9 @@ let sexp_of_t d = P.(sexp_of__t (from_t d))
 let of_yojson json = Ppx_deriving_yojson_runtime.(P.(_t_of_yojson json >|= to_t))
 let to_yojson level = P.(_t_to_yojson (from_t level))
 
+let t_of_python s = P.(to_t (_t_of_python s))
+let python_of_t d = P.(python_of__t (from_t d))
+
 type doc_view =
   [%import: Pp.doc_view]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp, yojson, python]
diff --git a/serlib/ser_pp.mli b/serlib/ser_pp.mli
index cf9073af..31cd83ee 100644
--- a/serlib/ser_pp.mli
+++ b/serlib/ser_pp.mli
@@ -22,8 +22,12 @@ val t_of_sexp : Sexp.t -> t
 val sexp_of_t : t -> Sexp.t
 val of_yojson : Yojson.Safe.t -> (t, string) Result.result
 val to_yojson : t -> Yojson.Safe.t
+val t_of_python : Py.Object.t -> t
+val python_of_t : t -> Py.Object.t
 
 val doc_view_of_sexp : Sexp.t -> doc_view
 val sexp_of_doc_view : doc_view -> Sexp.t
 val doc_view_of_yojson : Yojson.Safe.t -> (doc_view, string) Result.result
 val doc_view_to_yojson : doc_view -> Yojson.Safe.t
+val doc_view_of_python : Py.Object.t -> doc_view
+val python_of_doc_view : doc_view -> Py.Object.t
diff --git a/serlib/ser_ppextend.ml b/serlib/ser_ppextend.ml
index 41a812de..d5bc80c1 100644
--- a/serlib/ser_ppextend.ml
+++ b/serlib/ser_ppextend.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
 module Loc           = Ser_loc
 module Notation_term = Ser_notation_term
@@ -23,28 +24,28 @@ module Extend        = Ser_extend
 
 type ppbox =
   [%import: Ppextend.ppbox]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp,yojson,python]
 
 type ppcut =
   [%import: Ppextend.ppcut]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp,yojson,python]
 
 type pattern_quote_style =
   [%import: Ppextend.pattern_quote_style]
-  [@@deriving sexp, yojson]
+  [@@deriving sexp,yojson,python]
 
 type unparsing =
   [%import: Ppextend.unparsing]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type unparsing_rule =
   [%import: Ppextend.unparsing_rule]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type extra_unparsing_rules =
   [%import: Ppextend.extra_unparsing_rules]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 
 type notation_printing_rules =
   [%import: Ppextend.notation_printing_rules]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/ser_ppextend.mli b/serlib/ser_ppextend.mli
index b2d57ddc..933ab294 100644
--- a/serlib/ser_ppextend.mli
+++ b/serlib/ser_ppextend.mli
@@ -25,18 +25,14 @@ type ppcut = Ppextend.ppcut
 val ppcut_of_sexp : Sexp.t -> ppcut
 val sexp_of_ppcut : ppcut -> Sexp.t
 
-(* type unparsing = Ppextend.unparsing
- * val unparsing_of_sexp : Sexp.t -> unparsing
- * val sexp_of_unparsing : unparsing -> Sexp.t *)
-
 type unparsing_rule = Ppextend.unparsing_rule
 val unparsing_rule_of_sexp : Sexp.t -> unparsing_rule
 val sexp_of_unparsing_rule : unparsing_rule -> Sexp.t
+val unparsing_rule_of_python : Py.Object.t -> unparsing_rule
+val python_of_unparsing_rule : unparsing_rule -> Py.Object.t
 
 type extra_unparsing_rules = Ppextend.extra_unparsing_rules
-val extra_unparsing_rules_of_sexp : Sexp.t -> extra_unparsing_rules
-val sexp_of_extra_unparsing_rules : extra_unparsing_rules -> Sexp.t
+  [@@deriving sexp,python]
 
 type notation_printing_rules = Ppextend.notation_printing_rules
-val notation_printing_rules_of_sexp : Sexp.t -> notation_printing_rules
-val sexp_of_notation_printing_rules : notation_printing_rules -> Sexp.t
+  [@@deriving sexp,python]
diff --git a/serlib/ser_printer.ml b/serlib/ser_printer.ml
index 0c1ab9cc..d4ecaf11 100644
--- a/serlib/ser_printer.ml
+++ b/serlib/ser_printer.ml
@@ -19,4 +19,4 @@
 module Names = Ser_names
 type axiom =
   [%import: Printer.axiom]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/ser_proof_bullet.ml b/serlib/ser_proof_bullet.ml
index 48afa5d2..b55cec70 100644
--- a/serlib/ser_proof_bullet.ml
+++ b/serlib/ser_proof_bullet.ml
@@ -15,10 +15,11 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
 
 type t =
   [%import: Proof_bullet.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_range.ml b/serlib/ser_range.ml
index 60ab0986..d9614e2d 100644
--- a/serlib/ser_range.ml
+++ b/serlib/ser_range.ml
@@ -16,3 +16,5 @@
 type 'a t = 'a Range.t
 let sexp_of_t _ = Serlib_base.sexp_of_opaque ~typ:"Range.t"
 let t_of_sexp _ = Serlib_base.opaque_of_sexp ~typ:"Range.t"
+let python_of_t _ = Serlib_base.python_of_opaque ~typ:"Range.t"
+let t_of_python _ = Serlib_base.opaque_of_python ~typ:"Range.t"
diff --git a/serlib/ser_retroknowledge.ml b/serlib/ser_retroknowledge.ml
index da7a3043..5a3c6f2a 100644
--- a/serlib/ser_retroknowledge.ml
+++ b/serlib/ser_retroknowledge.ml
@@ -18,9 +18,8 @@ type retroknowledge =
 
 let sexp_of_retroknowledge = Serlib_base.sexp_of_opaque ~typ:"Retroknowledge.retroknowledge"
 let retroknowledge_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Retroknowledge.retroknowledge"
-
-(* type entry = 
- *   [%import: Retroknowledge.entry] *)
+let python_of_retroknowledge = Serlib_base.python_of_opaque ~typ:"Retroknowledge.retroknowledge"
+let retroknowledge_of_python = Serlib_base.opaque_of_python ~typ:"Retroknowledge.retroknowledge"
 
 type action = 
   [%import: Retroknowledge.action]
diff --git a/serlib/ser_retroknowledge.mli b/serlib/ser_retroknowledge.mli
index d0f515cb..84e2391f 100644
--- a/serlib/ser_retroknowledge.mli
+++ b/serlib/ser_retroknowledge.mli
@@ -18,8 +18,10 @@ type retroknowledge = Retroknowledge.retroknowledge
 
 val sexp_of_retroknowledge : retroknowledge -> Sexp.t
 val retroknowledge_of_sexp : Sexp.t -> retroknowledge
+val python_of_retroknowledge : retroknowledge -> Py.Object.t
+val retroknowledge_of_python : Py.Object.t -> retroknowledge
 
 type action = Retroknowledge.action
 
 val sexp_of_action : action -> Sexp.t
-val action_of_sexp : Sexp.t -> action
\ No newline at end of file
+val action_of_sexp : Sexp.t -> action
diff --git a/serlib/ser_rtree.ml b/serlib/ser_rtree.ml
index a04ccea3..6cfce2f6 100644
--- a/serlib/ser_rtree.ml
+++ b/serlib/ser_rtree.ml
@@ -15,6 +15,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_compare_lib.Builtin
 open Ppx_hash_lib.Std.Hash.Builtin
 
@@ -27,7 +28,7 @@ module RTreePierce = struct
     | Param of int * int
     | Node of 'a * 'a _t array
     | Rec of int * 'a _t array
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 include SerType.Pierce1(RTreePierce)
diff --git a/serlib/ser_safe_typing.ml b/serlib/ser_safe_typing.ml
index dd680326..0eddf063 100644
--- a/serlib/ser_safe_typing.ml
+++ b/serlib/ser_safe_typing.ml
@@ -16,9 +16,10 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module ONames = Names
 module CEphemeron = Ser_cEphemeron
@@ -33,17 +34,17 @@ module Univ = Ser_univ
 type certificate = {
   certif_struc : Declarations.structure_body;
   certif_univs : Univ.ContextSet.t;
-} [@@deriving sexp,yojson,hash,compare]
+} [@@deriving sexp,yojson,python,hash,compare]
 
 type side_effect = {
   from_env : certificate CEphemeron.key;
   seff_constant : Names.Constant.t;
   seff_body : Declarations.constant_body;
-} [@@deriving sexp,yojson,hash,compare]
+} [@@deriving sexp,yojson,python,hash,compare]
 
 module SeffOrd = struct
   type t = side_effect
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module SeffSet = Set.Make(SeffOrd)
@@ -53,7 +54,7 @@ module PC = struct
   (* t  private_constants *)
   type t = Safe_typing.private_constants
   type _t = { seff : side_effect list; elts : SerSeffSet.t }
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module B_ = SerType.Pierce(PC)
diff --git a/serlib/ser_sorts.ml b/serlib/ser_sorts.ml
index 15d732c6..4bde1017 100644
--- a/serlib/ser_sorts.ml
+++ b/serlib/ser_sorts.ml
@@ -17,7 +17,7 @@ module Univ = Ser_univ
 
 type family =
   [%import: Sorts.family]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module PierceSpec = struct
   type t = Sorts.t
@@ -26,11 +26,11 @@ module PierceSpec = struct
     | Prop
     | Set
     | Type of Univ.Universe.t
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 include SerType.Pierce(PierceSpec)
 
 type relevance =
   [%import: Sorts.relevance]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_sorts.mli b/serlib/ser_sorts.mli
index c224c9c6..2eb9f9e8 100644
--- a/serlib/ser_sorts.mli
+++ b/serlib/ser_sorts.mli
@@ -13,7 +13,7 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-include SerType.SJHC with type t = Sorts.t
+include SerType.SJPHC with type t = Sorts.t
 
-type family = Sorts.family [@@deriving sexp,yojson,hash,compare]
-type relevance = Sorts.relevance [@@deriving sexp,yojson,hash,compare]
+type family = Sorts.family [@@deriving sexp,yojson,python,hash,compare]
+type relevance = Sorts.relevance [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_stateid.ml b/serlib/ser_stateid.ml
index c50f004e..a0fc906d 100644
--- a/serlib/ser_stateid.ml
+++ b/serlib/ser_stateid.ml
@@ -14,13 +14,12 @@
 (************************************************************************)
 
 open Sexplib.Std
-
-module Self = struct
+open Ppx_python_runtime
 
 type t =
   [%import: Stateid.t]
 
-type _t = int [@@deriving sexp, yojson]
+type _t = int [@@deriving sexp, yojson, python]
 
 let _t_put stateid = (Stateid.to_int stateid)
 let _t_get stateid = Stateid.of_int stateid
@@ -30,6 +29,6 @@ let sexp_of_t stateid = sexp_of__t (_t_put stateid)
 
 let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get)
 let to_yojson level = _t_to_yojson (_t_put level)
-end
 
-include Self
+let t_of_python python    = _t_get (_t_of_python python)
+let python_of_t stateid = python_of__t (_t_put stateid)
diff --git a/serlib/ser_stateid.mli b/serlib/ser_stateid.mli
index baaf010f..eb5c3401 100644
--- a/serlib/ser_stateid.mli
+++ b/serlib/ser_stateid.mli
@@ -13,6 +13,4 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-module Self : SerType.SJ with type t = Stateid.t
-
-include module type of Self
+include SerType.SJP with type t = Stateid.t
diff --git a/serlib/ser_stdlib.ml b/serlib/ser_stdlib.ml
index 894d300f..78854a7a 100644
--- a/serlib/ser_stdlib.ml
+++ b/serlib/ser_stdlib.ml
@@ -29,9 +29,16 @@ let ref_of_yojson f x = Result.map (fun x -> ref x) (f x)
 let hash_fold_ref = hash_fold_ref_frozen
 let compare_ref = compare_ref
 
+let python_of_ref f (x : 'a ref) =
+  match x with | { contents } -> f contents
+
+let ref_of_python f x = ref (f x)
+
 module Lazy = struct
   type 'a t = 'a lazy_t
   [@@deriving sexp]
 end
 
 module Option = Stdlib.Option
+
+exception Not_found = Stdlib.Not_found
diff --git a/serlib/ser_stm.ml b/serlib/ser_stm.ml
index ea9b2bf0..82dc944c 100644
--- a/serlib/ser_stm.ml
+++ b/serlib/ser_stm.ml
@@ -14,21 +14,15 @@
 (************************************************************************)
 
 (* open Sexplib.Conv *)
+open Ppx_python_runtime
 
 module Stateid = Ser_stateid
 module Names   = Ser_names
 
-(* type interactive_top =
- *  [%import: Stm.interactive_top]
- *  [@@deriving sexp] *)
-
 type focus =
  [%import: Stm.focus]
- [@@deriving sexp]
+ [@@deriving sexp,python]
 
 type add_focus =
  [%import: Stm.add_focus]
- [@@deriving sexp]
-
- (* { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } *)
-
+ [@@deriving sexp,python]
diff --git a/serlib/ser_stm.mli b/serlib/ser_stm.mli
index edd8e9d7..f52b3221 100644
--- a/serlib/ser_stm.mli
+++ b/serlib/ser_stm.mli
@@ -16,16 +16,15 @@
 open Sexplib
 
 (* type interactive_top = Stm.interactive_top
- * 
+ *
  * val sexp_of_interactive_top : Stm.interactive_top -> Sexp.t
- * val interactive_top_of_sexp : Sexp.t -> Stm.interactive_top *)
+ * val interactive_top_of_sexp : Sexp.t -> Stm.interactive_top
+ * val python_of_interactive_top : Stm.interactive_top -> Py.Object.t
+ * val interactive_top_of_python : Py.Object.t -> Stm.interactive_top *)
 
 type focus = Stm.focus
 
 val sexp_of_focus : Stm.focus -> Sexp.t
 val focus_of_sexp : Sexp.t -> Stm.focus
 
-type add_focus = Stm.add_focus
-
-val sexp_of_add_focus : Stm.add_focus -> Sexp.t
-val add_focus_of_sexp : Sexp.t -> Stm.add_focus
+type add_focus = Stm.add_focus [@@deriving sexp,python]
diff --git a/serlib/ser_summary.ml b/serlib/ser_summary.ml
index 536d7b5f..285514e1 100644
--- a/serlib/ser_summary.ml
+++ b/serlib/ser_summary.ml
@@ -2,3 +2,5 @@ type frozen = Summary.frozen
 
 let frozen_of_sexp x = Serlib_base.opaque_of_sexp ~typ:"Summary.frozen" x
 let sexp_of_frozen x = Serlib_base.sexp_of_opaque ~typ:"Summary.frozen" x
+let frozen_of_python x = Serlib_base.opaque_of_python ~typ:"Summary.frozen" x
+let python_of_frozen x = Serlib_base.python_of_opaque ~typ:"Summary.frozen" x
diff --git a/serlib/ser_tok.ml b/serlib/ser_tok.ml
index 9c859208..1ccff409 100644
--- a/serlib/ser_tok.ml
+++ b/serlib/ser_tok.ml
@@ -14,12 +14,13 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
-module NumTok     = Ser_numTok
+module NumTok = Ser_numTok
 
 type t =
   [%import: Tok.t]
-  [@@deriving sexp]
+  [@@deriving sexp,yojson,python]
 
 type 'c p =
   [%import: 'c Tok.p]
@@ -37,6 +38,9 @@ type 'c _p =
   | PBULLET of string option
   | PQUOTATION of string
   | PEOI
-  [@@deriving of_sexp]
+  [@@deriving of_sexp,python]
 
 let p_of_sexp f x = Obj.magic (_p_of_sexp f x)
+
+let p_of_python f x = Obj.magic (_p_of_python f x)
+let python_of_p f x = python_of__p f (Obj.magic x)
diff --git a/serlib/ser_tok.mli b/serlib/ser_tok.mli
index b584293c..e07a456d 100644
--- a/serlib/ser_tok.mli
+++ b/serlib/ser_tok.mli
@@ -15,7 +15,7 @@
 
 open Sexplib
 
-type t = Tok.t
+include SerType.SJP with type t = Tok.t
 
 val t_of_sexp : Sexp.t -> t
 val sexp_of_t : t -> Sexp.t
@@ -23,3 +23,6 @@ val sexp_of_t : t -> Sexp.t
 type 'c p = 'c Tok.p
 val p_of_sexp : (Sexp.t -> 'c) -> Sexp.t -> 'c p
 val sexp_of_p : ('c -> Sexp.t) -> 'c p -> Sexp.t
+
+val p_of_python : (Py.Object.t -> 'c) -> Py.Object.t -> 'c p
+val python_of_p : ('c -> Py.Object.t) -> 'c p -> Py.Object.t
diff --git a/serlib/ser_typeclasses.ml b/serlib/ser_typeclasses.ml
index ce60bf8b..fca40edc 100644
--- a/serlib/ser_typeclasses.ml
+++ b/serlib/ser_typeclasses.ml
@@ -15,10 +15,11 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Conv
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
 
 type 'a hint_info_gen =
   [%import: 'a Typeclasses.hint_info_gen]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_typeclasses.mli b/serlib/ser_typeclasses.mli
index 6cf6c379..b122e029 100644
--- a/serlib/ser_typeclasses.mli
+++ b/serlib/ser_typeclasses.mli
@@ -15,4 +15,4 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-type 'a hint_info_gen = 'a Typeclasses.hint_info_gen [@@deriving sexp, yojson, hash,compare]
+type 'a hint_info_gen = 'a Typeclasses.hint_info_gen [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_uGraph.ml b/serlib/ser_uGraph.ml
index 296ff952..f787987d 100644
--- a/serlib/ser_uGraph.ml
+++ b/serlib/ser_uGraph.ml
@@ -21,7 +21,7 @@ module Univ = Ser_univ
 
 module Bound = struct
   type t = [%import: UGraph.Bound.t]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
 end
 
 type t = [%import: UGraph.t]
@@ -29,6 +29,9 @@ type t = [%import: UGraph.t]
 let sexp_of_t = Serlib_base.sexp_of_opaque ~typ:"UGraph.t"
 let t_of_sexp = Serlib_base.opaque_of_sexp ~typ:"UGraph.t"
 
+let python_of_t = Serlib_base.python_of_opaque ~typ:"UGraph.t"
+let t_of_python = Serlib_base.opaque_of_python ~typ:"UGraph.t"
+
 type univ_inconsistency =
   [%import: UGraph.univ_inconsistency]
   [@@deriving sexp]
diff --git a/serlib/ser_uGraph.mli b/serlib/ser_uGraph.mli
index fbed1d82..b61e3018 100644
--- a/serlib/ser_uGraph.mli
+++ b/serlib/ser_uGraph.mli
@@ -17,15 +17,10 @@ open Sexplib
 
 module Bound : sig
   type t = UGraph.Bound.t
-
-  val sexp_of_t : t -> Sexp.t
-  val t_of_sexp : Sexp.t -> t
+  [@@deriving sexp,python]
 end
 
-type t = UGraph.t
-
-val sexp_of_t : t -> Sexp.t
-val t_of_sexp : Sexp.t -> t
+type t = UGraph.t [@@deriving sexp,python]
 
 type univ_inconsistency = UGraph.univ_inconsistency
 
diff --git a/serlib/ser_uState.ml b/serlib/ser_uState.ml
index a5a21668..0d7d3d34 100644
--- a/serlib/ser_uState.ml
+++ b/serlib/ser_uState.ml
@@ -13,10 +13,11 @@
 (* Status: Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 type ('a,'b) gen_universe_decl =
   [%import: ('a,'b) UState.gen_universe_decl]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_uint63.ml b/serlib/ser_uint63.ml
index 9dd0fec8..c86cd6d3 100644
--- a/serlib/ser_uint63.ml
+++ b/serlib/ser_uint63.ml
@@ -15,8 +15,9 @@
 (************************************************************************)
 
 open Sexplib
+open Ppx_python_runtime
 
-type _t = string [@@deriving yojson]
+type _t = string [@@deriving yojson,python]
 let _t_put = Uint63.to_string
 let _t_get x = Uint63.of_int64 (Int64.of_string x)
 
@@ -33,3 +34,6 @@ let hash_fold_t st i =
 
 let compare i1 i2 =
   Ppx_compare_lib.Builtin.compare_int64 (Uint63.to_int64 i1) (Uint63.to_int64 i2)
+
+let t_of_python (x : Py.Object.t) : Uint63.t = _t_get (_t_of_python x)
+let python_of_t (x : Uint63.t) : Py.Object.t = python_of__t (_t_put x)
diff --git a/serlib/ser_univ.ml b/serlib/ser_univ.ml
index deb22700..4e75a59c 100644
--- a/serlib/ser_univ.ml
+++ b/serlib/ser_univ.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -23,7 +24,7 @@ module RawLevel = struct
 
   module UGlobal = struct
     type t = Names.DirPath.t * int
-    [@@deriving sexp, yojson, hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
   end
 
   type t =
@@ -32,7 +33,7 @@ module RawLevel = struct
   | Set
   | Level of UGlobal.t
   | Var of int
-  [@@deriving sexp, yojson, hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 end
 
@@ -42,7 +43,7 @@ module Level = struct
     type _t =
       { hash : int
       ; data : RawLevel.t
-      } [@@deriving sexp, yojson, hash,compare]
+      } [@@deriving sexp,yojson,python,hash,compare]
   end
 
   module PierceImp = SerType.Pierce(PierceSpec)
@@ -57,7 +58,7 @@ module Universe = struct
 
     type t = Univ.Universe.t
     type _t = (Level.t * int) list
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
   end
 
   include SerType.Pierce(PierceSpec)
@@ -69,7 +70,7 @@ module Variance = struct
 
   type t =
     [%import: Univ.Variance.t]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 end
 
@@ -81,7 +82,7 @@ type t =
 let hash_fold_array = hash_fold_array_frozen
 
 type _t = Instance of Level.t array
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let _instance_put instance            = Instance (Univ.Instance.to_array instance)
 let _instance_get (Instance instance) = Univ.Instance.of_array instance
@@ -97,15 +98,18 @@ let hash i = hash__t (Instance (Univ.Instance.to_array i))
 let hash_fold_t st i = hash_fold__t st (Instance (Univ.Instance.to_array i))
 let compare i1 i2 = compare__t (Instance (Univ.Instance.to_array i1)) (Instance (Univ.Instance.to_array i2))
 
+let t_of_python python     = _instance_get (_t_of_python python)
+let python_of_t instance = python_of__t (_instance_put instance)
+
 end
 
 type constraint_type =
   [%import: Univ.constraint_type]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type univ_constraint =
   [%import: Univ.univ_constraint]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module Constraints = Ser_cSet.Make(Univ.Constraints)(struct
     type t = univ_constraint
@@ -116,11 +120,13 @@ module Constraints = Ser_cSet.Make(Univ.Constraints)(struct
     let hash = hash_univ_constraint
     let hash_fold_t = hash_fold_univ_constraint
     let compare = compare_univ_constraint
+    let t_of_python = univ_constraint_of_python
+    let python_of_t = python_of_univ_constraint
   end)
 
 type 'a constrained =
   [%import: 'a Univ.constrained]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module UContext = struct
 
@@ -147,7 +153,7 @@ module AbstractContext = struct
 
     type t = Univ.AbstractContext.t
     type _t = Names.Name.t array constrained
-    [@@deriving sexp,yojson,hash,compare]
+    [@@deriving sexp,yojson,python,hash,compare]
   end
 
   include SerType.Pierce(ACPierceDef)
@@ -157,7 +163,7 @@ end
 module ContextSet = struct
   type t =
     [%import: Univ.ContextSet.t]
-    [@@deriving sexp, yojson, hash, compare]
+    [@@deriving sexp,yojson,python,hash,compare]
 end
 
 type 'a in_universe_context =
@@ -170,7 +176,7 @@ type 'a in_universe_context_set =
 
 type 'a puniverses =
   [%import: 'a Univ.puniverses]
-  [@@deriving sexp, yojson, hash, compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type explanation =
   [%import: Univ.explanation]
diff --git a/serlib/ser_univ.mli b/serlib/ser_univ.mli
index cffec495..67ad9fef 100644
--- a/serlib/ser_univ.mli
+++ b/serlib/ser_univ.mli
@@ -15,13 +15,13 @@
 
 open Sexplib
 
-module Level : SerType.SJHC with type t = Univ.Level.t
-module Universe : SerType.SJHC with type t = Univ.Universe.t
+module Level : SerType.SJPHC with type t = Univ.Level.t
+module Universe : SerType.SJPHC with type t = Univ.Universe.t
 
-module Variance : SerType.SJHC with type t = Univ.Variance.t
-module Instance : SerType.SJHC with type t = Univ.Instance.t
+module Variance : SerType.SJPHC with type t = Univ.Variance.t
+module Instance : SerType.SJPHC with type t = Univ.Instance.t
 
-type constraint_type = Univ.constraint_type [@@deriving sexp,yojson,hash,compare]
+type constraint_type = Univ.constraint_type [@@deriving sexp,yojson,python,hash,compare]
 
 type univ_constraint = Univ.univ_constraint
 
@@ -31,9 +31,9 @@ val sexp_of_univ_constraint : univ_constraint -> Sexp.t
 module Constraints : SerType.SJ with type t = Univ.Constraints.t
 module UContext : SerType.S with type t = Univ.UContext.t
 
-module AbstractContext : SerType.SJHC with type t = Univ.AbstractContext.t
+module AbstractContext : SerType.SJPHC with type t = Univ.AbstractContext.t
 
-module ContextSet : SerType.SJHC with type t = Univ.ContextSet.t
+module ContextSet : SerType.SJPHC with type t = Univ.ContextSet.t
 
 (** A value in a universe context (resp. context set). *)
 type 'a in_universe_context = 'a Univ.in_universe_context
@@ -45,7 +45,7 @@ val in_universe_context_set_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a in_universe
 val sexp_of_in_universe_context_set : ('a -> Sexp.t) -> 'a in_universe_context_set -> Sexp.t
 
 type 'a puniverses = 'a * Instance.t
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type explanation = Univ.explanation
 
diff --git a/serlib/ser_univNames.ml b/serlib/ser_univNames.ml
index 545b4d04..dfa6d8f2 100644
--- a/serlib/ser_univNames.ml
+++ b/serlib/ser_univNames.ml
@@ -13,12 +13,13 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
 
 module Names       = Ser_names
 
 type univ_name_list =
   [%import: UnivNames.univ_name_list]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_util.ml b/serlib/ser_util.ml
index ca9a2d49..a623c578 100644
--- a/serlib/ser_util.ml
+++ b/serlib/ser_util.ml
@@ -15,4 +15,4 @@
 
 type ('a,'b) union =
   [%import: ('a,'b) Util.union]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_util.mli b/serlib/ser_util.mli
index 3d1be2c5..e94e6ffe 100644
--- a/serlib/ser_util.mli
+++ b/serlib/ser_util.mli
@@ -13,4 +13,4 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-type ('a, 'b) union = ('a, 'b) Util.union [@@deriving sexp,yojson,hash,compare]
+type ('a, 'b) union = ('a, 'b) Util.union [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_vernacexpr.ml b/serlib/ser_vernacexpr.ml
index 7677c464..8144276f 100644
--- a/serlib/ser_vernacexpr.ml
+++ b/serlib/ser_vernacexpr.ml
@@ -13,9 +13,13 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Conv
+
+let python_of_unit _ = Py.Int.of_int 0
+let unit_of_python _ = ()
 
 module CUnix       = Ser_cUnix
 module Loc         = Ser_loc
@@ -49,273 +53,256 @@ module Impargs       = Ser_impargs
 module Typeclasses   = Ser_typeclasses
 
 type class_rawexpr = [%import: Vernacexpr.class_rawexpr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type goal_identifier = [%import: Vernacexpr.goal_identifier]
   [@@deriving sexp]
 
 type scope_name      = [%import: Vernacexpr.scope_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type goal_reference =
   [%import: Vernacexpr.goal_reference]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type printable =
   [%import: Vernacexpr.printable]
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type vernac_cumulative =
- *   [%import: Vernacexpr.vernac_cumulative]
- *   [@@deriving sexp,yojson] *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type glob_search_where =
   [%import: Vernacexpr.glob_search_where]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type search_item =
   [%import: Vernacexpr.search_item]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type search_request =
   [%import: Vernacexpr.search_request]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type searchable =
   [%import: Vernacexpr.searchable]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type locatable = [%import: Vernacexpr.locatable]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type showable =  [%import: Vernacexpr.showable]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type comment =
   [%import: Vernacexpr.comment]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type search_restriction =  [%import: Vernacexpr.search_restriction]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* type rec_flag          = [%import: Vernacexpr.rec_flag          ] [@@deriving sexp,yojson] *)
-type verbose_flag      = [%import: Vernacexpr.verbose_flag      ] [@@deriving sexp,yojson,hash,compare]
-type coercion_flag     = [%import: Vernacexpr.coercion_flag     ] [@@deriving sexp,yojson,hash,compare]
-(* type inductive_flag    = [%import: Vernacexpr.inductive_flag    ] [@@deriving sexp,yojson,hash,compare] *)
-type instance_flag     = [%import: Vernacexpr.instance_flag     ] [@@deriving sexp,yojson,hash,compare]
-type export_flag       = [%import: Vernacexpr.export_flag       ] [@@deriving sexp,yojson,hash,compare]
-(* type onlyparsing_flag  = [%import: Vernacexpr.onlyparsing_flag  ] [@@deriving sexp,yojson,hash,compare] *)
-type locality_flag     = [%import: Vernacexpr.locality_flag     ] [@@deriving sexp,yojson,hash,compare]
-(* type obsolete_locality = [%import: Vernacexpr.obsolete_locality ] [@@deriving sexp] *)
+type verbose_flag      = [%import: Vernacexpr.verbose_flag      ] [@@deriving sexp,yojson,python,hash,compare]
+type coercion_flag     = [%import: Vernacexpr.coercion_flag     ] [@@deriving sexp,yojson,python,hash,compare]
+(* type inductive_flag    = [%import: Vernacexpr.inductive_flag    ] [@@deriving sexp,yojson,python,hash,compare] *)
+type instance_flag     = [%import: Vernacexpr.instance_flag     ] [@@deriving sexp,yojson,python,hash,compare]
+type export_flag       = [%import: Vernacexpr.export_flag       ] [@@deriving sexp,yojson,python,hash,compare]
+(* type onlyparsing_flag  = [%import: Vernacexpr.onlyparsing_flag  ] [@@deriving sexp,yojson,python,hash,compare] *)
+type locality_flag     = [%import: Vernacexpr.locality_flag     ] [@@deriving sexp,yojson,python,hash,compare]
 
 type option_setting =
   [%import: Vernacexpr.option_setting]
-  [@@deriving sexp,yojson,hash,compare]
-
-(* type option_ref_value =
- *   [%import: Vernacexpr.option_ref_value]
- *   [@@deriving sexp,yojson,hash,compare] *)
-
-(* type plident =
- *   [%import: Vernacexpr.plident ]
- *   [@@deriving sexp] *)
-
-(* type sort_expr =
- *   [%import: Vernacexpr.sort_expr]
- *   [@@deriving sexp,yojson,hash,compare] *)
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type definition_expr =
   [%import: Vernacexpr.definition_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type import_categories =
   [%import: Vernacexpr.import_categories]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type infix_flag =
   [%import: Vernacexpr.infix_flag]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type notation_format =
   [%import: Vernacexpr.notation_format]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type syntax_modifier =
   [%import: Vernacexpr.syntax_modifier]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type decl_notation =
   [%import: Vernacexpr.decl_notation]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a fix_expr_gen =
   [%import: 'a Vernacexpr.fix_expr_gen]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type fixpoint_expr =
   [%import: Vernacexpr.fixpoint_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cofixpoint_expr =
   [%import: Vernacexpr.cofixpoint_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type local_decl_expr =
   [%import: Vernacexpr.local_decl_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type inductive_kind =
   [%import: Vernacexpr.inductive_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type simple_binder =
   [%import: Vernacexpr.simple_binder]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type class_binder =
   [%import: Vernacexpr.class_binder]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type 'a with_coercion =
   [%import: 'a Vernacexpr.with_coercion]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 (* type 'a with_instance =
  *   [%import: 'a Vernacexpr.with_instance]
- *   [@@deriving sexp,yojson,hash,compare] *)
+ *   [@@deriving sexp,yojson,python,hash,compare] *)
 
 (* type 'a with_notation =
  *   [%import: 'a Vernacexpr.with_notation]
- *   [@@deriving sexp,yojson,hash,compare] *)
+ *   [@@deriving sexp,yojson,python,hash,compare] *)
 
 (* type 'a with_priority =
  *   [%import: 'a Vernacexpr.with_priority]
- *   [@@deriving sexp,yojson,hash,compare] *)
+ *   [@@deriving sexp,yojson,python,hash,compare] *)
 
 type constructor_expr =
   [%import: Vernacexpr.constructor_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type record_field_attr =
   [%import: Vernacexpr.record_field_attr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type constructor_list_or_record_decl_expr =
   [%import: Vernacexpr.constructor_list_or_record_decl_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type inductive_params_expr =
   [%import: Vernacexpr.inductive_params_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type inductive_expr =
   [%import: Vernacexpr.inductive_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type one_inductive_expr =
   [%import: Vernacexpr.one_inductive_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type proof_expr =
   [%import: Vernacexpr.proof_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type opacity_flag =
   [%import: Vernacexpr.opacity_flag]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type proof_end =
   [%import: Vernacexpr.proof_end]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type one_import_filter_name =
   [%import: Vernacexpr.one_import_filter_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type import_filter_expr =
   [%import: Vernacexpr.import_filter_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type scheme_type =
   [%import: Vernacexpr.scheme_type]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type equality_scheme_type =
   [%import: Vernacexpr.equality_scheme_type]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type scheme =
   [%import: Vernacexpr.scheme]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type section_subset_expr =
   [%import: Vernacexpr.section_subset_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type extend_name =
   [%import: Vernacexpr.extend_name]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type register_kind =
   [%import: Vernacexpr.register_kind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type module_ast_inl =
   [%import: Vernacexpr.module_ast_inl]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type export_with_cats =
   [%import: Vernacexpr.export_with_cats]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type module_binder =
   [%import: Vernacexpr.module_binder]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type typeclass_constraint =
   [%import: Vernacexpr.typeclass_constraint]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type discharge =
   [%import: Vernacexpr.discharge]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type arguments_modifier =
   [%import: Vernacexpr.arguments_modifier]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type vernac_one_argument_status =
   [%import: Vernacexpr.vernac_one_argument_status]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type vernac_argument_status =
   [%import: Vernacexpr.vernac_argument_status]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type hint_info_expr =
   [%import: Vernacexpr.hint_info_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type reference_or_constr =
   [%import: Vernacexpr.reference_or_constr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type hints_expr =
   [%import: Vernacexpr.hints_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type vernac_expr =
   [%import: Vernacexpr.vernac_expr]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type control_flag =
   [%import: Vernacexpr.control_flag]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type vernac_control_r =
   [%import: Vernacexpr.vernac_control_r]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type vernac_control =
   [%import: Vernacexpr.vernac_control]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli
index 3a14be30..b27959e2 100644
--- a/serlib/ser_vernacexpr.mli
+++ b/serlib/ser_vernacexpr.mli
@@ -291,4 +291,4 @@ type vernac_control_r =
 
 type vernac_control =
   [%import: Vernacexpr.vernac_control]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_vmbytecodes.ml b/serlib/ser_vmbytecodes.ml
index 55701a28..b73e428a 100644
--- a/serlib/ser_vmbytecodes.ml
+++ b/serlib/ser_vmbytecodes.ml
@@ -16,6 +16,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -26,8 +27,8 @@ let hash_fold_array = hash_fold_array_frozen
 
 type fv_elem =
   [%import: Vmbytecodes.fv_elem]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type fv =
   [%import: Vmbytecodes.fv]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_vmemitcodes.ml b/serlib/ser_vmemitcodes.ml
index 072417d7..9cd8859b 100644
--- a/serlib/ser_vmemitcodes.ml
+++ b/serlib/ser_vmemitcodes.ml
@@ -17,6 +17,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -31,25 +32,25 @@ type reloc_info =
   | Reloc_const of Vmvalues.structured_constant
   | Reloc_getglobal of Names.Constant.t
   | Reloc_caml_prim of CPrimitives.t
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 let hash_fold_array = hash_fold_array_frozen
 
 type patches = {
   reloc_infos : (reloc_info * int array) array;
-} [@@deriving sexp,yojson,hash,compare]
+} [@@deriving sexp,yojson,python,hash,compare]
 
 type emitcodes = string
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type _to_patch = emitcodes * patches
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 module PierceToPatch = struct
 
   type t = Vmemitcodes.to_patch
   type _t = _to_patch
-   [@@deriving sexp,yojson,hash,compare]
+   [@@deriving sexp,yojson,python,hash,compare]
 
 end
 
@@ -58,6 +59,8 @@ module B = SerType.Pierce(PierceToPatch)
 type to_patch = B.t
 let sexp_of_to_patch = B.sexp_of_t
 let to_patch_of_sexp = B.t_of_sexp
+let python_of_to_patch = B.python_of_t
+let to_patch_of_python = B.t_of_python
 let to_patch_of_yojson = B.of_yojson
 let to_patch_to_yojson = B.to_yojson
 (* let hash_to_patch = B.hash *)
@@ -66,4 +69,4 @@ let compare_to_patch = B.compare
 
 type body_code =
   [%import: Vmemitcodes.body_code]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_vmemitcodes.mli b/serlib/ser_vmemitcodes.mli
index 220be42d..5803cf32 100644
--- a/serlib/ser_vmemitcodes.mli
+++ b/serlib/ser_vmemitcodes.mli
@@ -17,9 +17,4 @@
 (************************************************************************)
 
 type body_code = Vmemitcodes.body_code
- [@@deriving sexp,yojson,hash,compare]
-
-(* type to_patch_substituted = Vmemitcodes.to_patch_substituted
- *
- * val sexp_of_to_patch_substituted : to_patch_substituted -> Sexp.t
- * val to_patch_substituted_of_sexp : Sexp.t -> to_patch_substituted *)
+ [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_vmvalues.ml b/serlib/ser_vmvalues.ml
index c363281c..d2a58fd6 100644
--- a/serlib/ser_vmvalues.ml
+++ b/serlib/ser_vmvalues.ml
@@ -14,7 +14,8 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-open Sexplib.Conv
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -26,7 +27,7 @@ module Float64 = Ser_float64
 
 type tag =
   [%import: Vmvalues.tag]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module OpaqueSV = struct
   type t = Vmvalues.structured_values
@@ -38,6 +39,8 @@ module B = SerType.Opaque(OpaqueSV)
 type structured_values = B.t
 let sexp_of_structured_values = B.sexp_of_t
 let structured_values_of_sexp = B.t_of_sexp
+let python_of_structured_values = B.python_of_t
+let structured_values_of_python = B.t_of_python
 let structured_values_of_yojson = B.of_yojson
 let structured_values_to_yojson = B.to_yojson
 (* let hash_structured_values = B.hash *)
@@ -46,14 +49,14 @@ let compare_structured_values = B.compare
 
 type structured_constant =
   [%import: Vmvalues.structured_constant]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 let hash_fold_array = hash_fold_array_frozen
 
 type reloc_table =
   [%import: Vmvalues.reloc_table]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type annot_switch =
   [%import: Vmvalues.annot_switch]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/ser_vmvalues.mli b/serlib/ser_vmvalues.mli
index dbe5e43c..b95312e0 100644
--- a/serlib/ser_vmvalues.mli
+++ b/serlib/ser_vmvalues.mli
@@ -22,10 +22,10 @@ val tag_of_sexp : Sexp.t -> tag
 val sexp_of_tag : tag -> Sexp.t
 
 type structured_constant = Vmvalues.structured_constant
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type reloc_table = Vmvalues.reloc_table
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
 
 type annot_switch = Vmvalues.annot_switch
- [@@deriving sexp,yojson,hash,compare]
+ [@@deriving sexp,yojson,python,hash,compare]
diff --git a/serlib/serlib_base.ml b/serlib/serlib_base.ml
index 2ee526d9..4b86216d 100644
--- a/serlib/serlib_base.ml
+++ b/serlib/serlib_base.ml
@@ -43,7 +43,16 @@ let opaque_to_yojson ~typ _obj =
   else
     `String ("["^typ^": ABSTRACT]")
 
+let opaque_of_python ~typ _obj =
+  raise (Ser_error ("["^typ^": ABSTRACT / cannot deserialize]"))
+
+let python_of_opaque ~typ _obj =
+  let msg = "["^typ^": ABSTRACT]" in
+  if !exn_on_opaque then
+    raise (Ser_error msg)
+  else
+    Py.String.of_string ("["^typ^": ABSTRACT]")
+
 let hash_opaque ~typ:_ x = Hashtbl.hash x
 let hash_fold_opaque ~typ st x = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int st (hash_opaque ~typ x)
 let compare_opaque ~typ:_ x y = Stdlib.compare x y
-
diff --git a/serlib/serlib_base.mli b/serlib/serlib_base.mli
index c4c63838..ceeba014 100644
--- a/serlib/serlib_base.mli
+++ b/serlib/serlib_base.mli
@@ -25,6 +25,9 @@ val opaque_of_sexp : typ:string -> Sexp.t -> 'a
 val opaque_of_yojson : typ:string -> Yojson.Safe.t -> ('a, string) Result.t
 val opaque_to_yojson : typ:string -> 'a -> Yojson.Safe.t
 
+val python_of_opaque : typ:string -> 'a -> Py.Object.t
+val opaque_of_python : typ:string -> Py.Object.t -> 'a
+
 val hash_opaque : typ:string -> 'a -> Ppx_hash_lib.Std.Hash.hash_value
 val hash_fold_opaque : typ:string -> Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state
 
diff --git a/sertop/dune b/sertop/dune
index bf48adb3..5290cda0 100644
--- a/sertop/dune
+++ b/sertop/dune
@@ -2,17 +2,32 @@
  (name sertop)
  (public_name coq-serapi.sertop_v8_12)
  (modules :standard \ sertop_bin sercomp sertok sername sertop_js sertop_async)
- (preprocess (staged_pps ppx_import ppx_sexp_conv))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python))
  (libraries findlib.dynload cmdliner serapi serlib serlib_ltac))
 
 (executables
  (public_names sertop sercomp sertok sername)
  (names sertop_bin sercomp sertok sername)
  (modules sertop_bin sercomp sertok sername)
- (preprocess (staged_pps ppx_import ppx_sexp_conv))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python))
  (link_flags -linkall)
  (libraries sertop))
 
+(executable
+ (name sertop_js)
+ (modules sertop_async sertop_js)
+ (modes js)
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python))
+ (js_of_ocaml
+  (javascript_files
+    ../jscoq/coq-libjs/mutex.js
+    ../jscoq/coq-libjs/unix.js
+    ../jscoq/coq-libjs/str.js
+    ../jscoq/coq-libjs/coq_vm.js)
+  (flags :standard --dynlink +dynlink.js +toplevel.js))
+ (link_flags -linkall -noautolink -no-check-prims)
+ (libraries sertop ppx_deriving_yojson.runtime zarith_stubs_js jscoq_lib))
+
 (rule
  (targets ser_version.ml)
  (action (write-file %{targets} "let ser_git_version = \"%{version:coq-serapi}\";;")))
diff --git a/sertop/sertop_pyser.ml b/sertop/sertop_pyser.ml
new file mode 100644
index 00000000..37d30dd1
--- /dev/null
+++ b/sertop/sertop_pyser.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq serialization API/Plugin                                         *)
+(* Copyright 2016-2018 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+(* Status: Very Experimental                                            *)
+(************************************************************************)
+
+open Ppx_python_runtime
+
+open Serlib
+
+type ser_printer =
+  | SP_Sertop                   (* sertop custom printer (UTF-8, stronger quoting) *)
+  | SP_Mach                     (* sexplib mach  printer *)
+  | SP_Human                    (* sexplib human printer *)
+
+let select_printer pr = match pr with
+  | SP_Sertop -> Sertop_util.pp_sertop
+  | SP_Mach   -> Sexplib.Sexp.pp
+  | SP_Human  -> Sexplib.Sexp.pp_hum
+
+module SP = Serapi.Serapi_protocol
+
+(******************************************************************************)
+(* Exception Registration                                                     *)
+(******************************************************************************)
+
+(* We play slow for now *)
+let _ =
+  (* XXX Finish this *)
+  let open Sexplib in
+  let open Sexplib.Conv in
+  let open Sexplib.Sexp in
+  let sexp_of_std_ppcmds pp = Atom (Pp.string_of_ppcmds pp) in
+  Conv.Exn_converter.add [%extension_constructor SP.NoSuchState] (function
+      (* Own things *)
+      | SP.NoSuchState sid ->
+        List [Atom "NoSuchState"; Ser_stateid.sexp_of_t sid]
+      | _ -> assert false);
+  Conv.Exn_converter.add [%extension_constructor CErrors.UserError] (function
+      (* Errors *)
+      | CErrors.UserError(msg) ->
+        List [Atom "CErrors.UserError"; List [sexp_of_std_ppcmds msg]]
+      | _ -> assert false);
+  Conv.Exn_converter.add [%extension_constructor DeclareUniv.AlreadyDeclared] (function
+      | DeclareUniv.AlreadyDeclared (msg, id) ->
+        List [Atom "Declare.AlreadyDeclared"; List [sexp_of_option sexp_of_string msg; Ser_names.Id.sexp_of_t id]]
+      | _ -> assert false);
+  Conv.Exn_converter.add [%extension_constructor Pretype_errors.PretypeError] (function
+      (* Pretype Errors XXX what to do with _env, _envmap *)
+      | Pretype_errors.PretypeError(_env, _evmap, pterr) ->
+        List [Atom "Pretype_errors.PretypeError";
+              List [Ser_pretype_errors.sexp_of_pretype_error pterr]]
+      | _ -> assert false);
+  (* Conv.Exn_converter.add [%extension_constructor Proof_global.NoCurrentProof] (function
+   *     | Proof_global.NoCurrentProof ->
+   *       Atom "NoCurrentProof"
+   *     | _ -> assert false) *)
+(* Private... request Coq devs to make them public?
+      | Errors.Anomaly(msgo, pp) ->
+        Some (List [Atom "Anomaly"; sexp_of_option sexp_of_string msgo; sexp_of_std_ppcmds pp])
+*)
+
+(******************************************************************************)
+(* Serialization of the Protocol                                              *)
+(******************************************************************************)
+
+module Loc      = Ser_loc
+module CAst     = Ser_cAst
+module Pp       = Ser_pp
+module Names    = Ser_names
+module Environ  = Ser_environ
+module Goptions = Ser_goptions
+module Stateid  = Ser_stateid
+module Evar     = Ser_evar
+module Context  = Ser_context
+module Feedback = Ser_feedback
+module Libnames = Ser_libnames
+module Globnames = Ser_globnames
+module Impargs    = Ser_impargs
+module Constr     = Ser_constr
+module Constrexpr = Ser_constrexpr
+module Proof      = Ser_proof
+module Tok        = Ser_tok
+module Ppextend   = Ser_ppextend
+module Notation_gram = Ser_notation_gram
+module Genarg     = Ser_genarg
+module Loadpath   = Ser_loadpath
+module Printer    = Ser_printer
+
+(* Alias fails due to the [@@default in protocol] *)
+(* module Stm        = Ser_stm *)
+module Ser_stm    = Ser_stm
+
+module Ltac_plugin = struct
+  module Tacenv       = Serlib_ltac.Ser_tacenv
+  module Profile_ltac = Serlib_ltac.Ser_profile_ltac
+  module Tacexpr      = Serlib_ltac.Ser_tacexpr
+end
+
+module Notation   = Ser_notation
+module Xml_datatype = Ser_xml_datatype
+module Notation_term = Ser_notation_term
+module Vernacexpr   = Ser_vernacexpr
+module Declarations = Ser_declarations
+module Lib = Ser_lib
+module Nametab = Ser_nametab
+module Coqargs = Ser_coqargs
+
+(* XXX: hack!! *)
+[@@@ocaml.warning "-38"]
+exception Not_found_s = Base.Not_found_s
+(* XXX: end hack!! *)
+
+module Serapi = struct
+module Serapi_goals = struct
+
+  type 'a hyp =
+    [%import: 'a Serapi.Serapi_goals.hyp]
+    [@@deriving python]
+
+  type info =
+    [%import: Serapi.Serapi_goals.info]
+    [@@deriving python]
+
+  type 'a reified_goal =
+    [%import: 'a Serapi.Serapi_goals.reified_goal]
+    [@@deriving python]
+
+  type 'a ser_goals =
+    [%import: 'a Serapi.Serapi_goals.ser_goals]
+    [@@deriving python]
+
+end
+
+module Serapi_assumptions = struct
+type ax_ctx =
+  [%import: Serapi.Serapi_assumptions.ax_ctx]
+  [@@deriving python]
+
+type t =
+  [%import: Serapi.Serapi_assumptions.t]
+  [@@deriving python]
+
+end
+
+module Serapi_protocol = Serapi.Serapi_protocol
+
+end
+
+(* Serialization to sexp *)
+type coq_object =
+  [%import: Serapi.Serapi_protocol.coq_object]
+  [@@deriving python]
+
+exception AnswerExn of Py.Object.t
+let exn_of_python sexp = AnswerExn sexp
+let python_of_exn _ = Py.none
+
+type print_format =
+  [%import: Serapi.Serapi_protocol.print_format]
+  [@@deriving python]
+
+type format_opt =
+  [%import: Serapi.Serapi_protocol.format_opt]
+  [@@deriving python]
+
+type print_opt =
+  [%import: Serapi.Serapi_protocol.print_opt]
+  [@@deriving python]
+
+type query_pred =
+  [%import: Serapi.Serapi_protocol.query_pred]
+  [@@deriving python]
+
+type query_opt =
+  [%import: Serapi.Serapi_protocol.query_opt
+  [@with
+     Sexplib.Conv.sexp_list   := sexp_list;
+     Sexplib.Conv.sexp_option := sexp_option;
+  ]]
+  [@@deriving python]
+
+type query_cmd =
+  [%import: Serapi.Serapi_protocol.query_cmd]
+  [@@deriving python]
+
+type cmd_tag =
+  [%import: Serapi.Serapi_protocol.cmd_tag]
+  [@@deriving python]
+
+type location =
+  [%import: Printexc.location]
+  [@@deriving python]
+
+type raw_backtrace = Printexc.raw_backtrace
+let raw_backtrace_of_python _ = Printexc.get_raw_backtrace ()
+
+type slot_rep = {
+  slot_loc : location option;
+  slot_idx : int;
+  slot_str : string option;
+} [@@deriving python]
+
+let to_slot_rep idx bs = {
+  slot_loc = Printexc.Slot.location bs;
+  slot_idx = idx;
+  slot_str = Printexc.Slot.format idx bs;
+}
+
+let python_of_backtrace_slot idx bs =
+  python_of_slot_rep (to_slot_rep idx bs)
+
+(*
+let sexp_of_raw_backtrace (bt : Printexc.raw_backtrace) : Sexp.t =
+  let bt = Printexc.backtrace_slots bt in
+  let bt = Option.map Array.(mapi sexp_of_backtrace_slot) bt in
+  let bt = sexp_of_option (sexp_of_array (fun x -> x)) bt in
+  Sexp.(List [Atom "Backtrace"; bt])
+*)
+
+let python_of_raw_backtrace (_bt : Printexc.raw_backtrace) : Py.Object.t =
+  Ppx_python_runtime.python_of_bool false
+
+module ExnInfo = struct
+  type t =
+    [%import: Serapi.Serapi_protocol.ExnInfo.t
+    [@with
+       Stm.focus := Ser_stm.focus;
+       Printexc.raw_backtrace := raw_backtrace;
+       Stdlib.Printexc.raw_backtrace := raw_backtrace;
+    ]]
+    [@@deriving python]
+end
+
+type answer_kind =
+  [%import: Serapi.Serapi_protocol.answer_kind
+  [@with
+    Exninfo.t := Exninfo.t;
+    Stm.add_focus := Ser_stm.add_focus;
+  ]]
+  [@@deriving python]
+
+type feedback_content =
+  [%import: Serapi.Serapi_protocol.feedback_content]
+  [@@deriving python]
+
+type feedback =
+  [%import: Serapi.Serapi_protocol.feedback]
+  [@@deriving python]
+
+type answer =
+  [%import: Serapi.Serapi_protocol.answer]
+  [@@deriving python]
+
+type add_opts =
+  [%import: Serapi.Serapi_protocol.add_opts
+  [@with
+     Sexplib.Conv.sexp_option := sexp_option;
+  ]]
+  [@@deriving python]
+
+type newdoc_opts =
+  [%import: Serapi.Serapi_protocol.newdoc_opts
+  [@with
+     Stm.interactive_top      := Ser_stm.interactive_top;
+     Sexplib.Conv.sexp_list   := sexp_list;
+     Sexplib.Conv.sexp_option := sexp_option;
+  ]]
+  [@@deriving python]
+
+type save_opts =
+  [%import: Serapi.Serapi_protocol.save_opts]
+  [@@deriving python]
+
+type parse_opt =
+  [%import: Serapi.Serapi_protocol.parse_opt
+  [@with
+     Sexplib.Conv.sexp_option := sexp_option;
+  ]]
+  [@@deriving python]
+
+type cmd =
+  [%import: Serapi.Serapi_protocol.cmd]
+  [@@deriving python]
+
+type tagged_cmd =
+  [%import: Serapi.Serapi_protocol.tagged_cmd]
+  [@@deriving python]
+
+type sentence = Sentence of Tok.t CAst.t list
+  [@@deriving python]