Adapt to flattenting of global_declaration indirection (Coq PR #19185).

ejgallego · Jun 25, 2024 · 624509b · 624509b
1 parent d3e998b
commit 624509b
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 10 deletions.
diff --git a/serlib/ser_safe_typing.ml b/serlib/ser_safe_typing.ml
@@ -78,7 +78,3 @@ let _effect_entry_of_sexp (_f : Sexp.t -> 'a) (x : Sexp.t) : 'a effect_entry =
   | _ ->
     Sexplib.Conv_error.no_variant_match ()
 *)
-
-type global_declaration =
-  [%import: Safe_typing.global_declaration]
-  [@@deriving sexp]
diff --git a/serlib/ser_safe_typing.mli b/serlib/ser_safe_typing.mli
@@ -16,11 +16,5 @@
 (* Written by: Emilio J. Gallego Arias and others                       *)
 (************************************************************************)
 
-open Sexplib
-
 type private_constants = Safe_typing.private_constants
   [@@deriving sexp,yojson,hash,compare]
-
-type global_declaration = Safe_typing.global_declaration
-val global_declaration_of_sexp : Sexp.t -> global_declaration
-val sexp_of_global_declaration : global_declaration -> Sexp.t