Merge pull request #796 from herbelin/main+adapt-coq-pr19185-flatteni…

…ng-global_declaration Adapt to Coq PR #19185: flattenting of global_declaration indirection.
ejgallego · Jun 26, 2024 · 3282609 · 3282609
2 parents d3e998b + 624509b
commit 3282609
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