From 94447f99e8dd9ee8ce06c14cf521360b53ff2beb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 May 2023 17:11:50 +0200 Subject: [PATCH] Adapt to coq/coq#17575 (ltac2val in ltac1) --- serlib/plugins/ltac2/ser_tac2env.ml | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/serlib/plugins/ltac2/ser_tac2env.ml b/serlib/plugins/ltac2/ser_tac2env.ml index 44dc5a29..8143b04a 100644 --- a/serlib/plugins/ltac2/ser_tac2env.ml +++ b/serlib/plugins/ltac2/ser_tac2env.ml @@ -11,7 +11,7 @@ module CAst = Ser_cAst module Names = Ser_names module Tac2expr = Ser_tac2expr -module WL2 = struct +module WL2in1 = struct type raw = Tac2expr.uid CAst.t list * Tac2expr.raw_tacexpr [@@deriving sexp,hash,compare] type glb = Tac2expr.uid list * Tac2expr.glb_tacexpr @@ -20,7 +20,18 @@ module WL2 = struct [@@deriving sexp,hash,compare] end -let ser_wit_ltac2 = let module M = Ser_genarg.GS(WL2) in M.genser +let ser_wit_ltac2in1 = let module M = Ser_genarg.GS(WL2in1) in M.genser + +module WL2in1V = struct + type raw = Tac2expr.uid CAst.t list * Tac2expr.raw_tacexpr + [@@deriving sexp,hash,compare] + type glb = Tac2expr.glb_tacexpr + [@@deriving sexp,hash,compare] + type top = Util.Empty.t + [@@deriving sexp,hash,compare] +end + +let ser_wit_ltac2in1_val = let module M = Ser_genarg.GS(WL2in1V) in M.genser module WLC2 = struct type raw = Tac2expr.raw_tacexpr @@ -56,7 +67,8 @@ end let ser_wit_ltac2_val = let module M = Ser_genarg.GS(WLV2) in M.genser let register () = - Ser_genarg.register_genser Tac2env.wit_ltac2 ser_wit_ltac2; + Ser_genarg.register_genser Tac2env.wit_ltac2in1 ser_wit_ltac2in1; + Ser_genarg.register_genser Tac2env.wit_ltac2in1_val ser_wit_ltac2in1_val; Ser_genarg.register_genser Tac2env.wit_ltac2_constr ser_wit_ltac2_constr; Ser_genarg.register_genser Tac2env.wit_ltac2_quotation ser_wit_ltac2_quotation; Ser_genarg.register_genser Tac2env.wit_ltac2_val ser_wit_ltac2_val;