From 624509b3f4f2ef6107a98be2848880a1318f16e9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 25 Jun 2024 17:17:50 +0200 Subject: [PATCH] Adapt to flattenting of global_declaration indirection (Coq PR #19185). --- serlib/ser_safe_typing.ml | 4 ---- serlib/ser_safe_typing.mli | 6 ------ 2 files changed, 10 deletions(-) diff --git a/serlib/ser_safe_typing.ml b/serlib/ser_safe_typing.ml index 4f5cdb03..5450a722 100644 --- 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 index 1613aad1..564b2ce4 100644 --- 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