Merge pull request #333 from SkySkimmer/ltac2in1

Adapt to coq/coq#17575 (ltac2val in ltac1)
ejgallego · Jun 1, 2023 · 5b11174 · 5b11174
2 parents 82620ec + 94447f9
commit 5b11174
Showing 1 changed file with 15 additions and 3 deletions.
diff --git 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;