Adapt to coq/coq#20315 (may_eval type moved)

ejgallego · Mar 3, 2025 · 957a502 · 957a502
1 parent 62984e6
commit 957a502
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 8 deletions.
diff --git a/serlib/plugins/ltac/ser_tacexpr.ml b/serlib/plugins/ltac/ser_tacexpr.ml
@@ -131,6 +131,9 @@ type ml_tactic_entry =
   [%import: Ltac_plugin.Tacexpr.ml_tactic_entry]
   [@@deriving sexp,yojson,hash,compare]
 
+type ('a, 'b, 'c, 'd) may_eval = [%import: ('a,'b,'c,'d) Ltac_plugin.Tacexpr.may_eval]
+  [@@deriving sexp,yojson,hash,compare]
+
 (* type dyn = Ser_Dyn [@@deriving sexp] *)
 (* let to_dyn _   = Ser_Dyn *)
 (* let from_dyn _ = fst (Dyn.create "dyn_tac") 0 *)
@@ -167,7 +170,7 @@ type ('trm, 'dtrm, 'pat, 'redpat, 'cst, 'ref, 'nam, 'occvar, 'tacexpr, 'lev) gen
 
 and ('trm, 'dtrm, 'pat, 'redpat, 'cst, 'ref, 'nam, 'occvar, 'tacexpr, 'lev) gen_tactic_arg =
   | TacGeneric     of string option * 'lev Genarg.generic_argument
-  | ConstrMayEval  of ('trm,'cst,'redpat,'occvar) Genredexpr.may_eval
+  | ConstrMayEval  of ('trm,'cst,'redpat,'occvar) may_eval
   | Reference      of 'ref
   | TacCall        of ('ref *
       ('trm, 'dtrm, 'pat, 'redpat, 'cst, 'ref, 'nam, 'occvar, 'tacexpr, 'lev) gen_tactic_arg list) CAst.t

diff --git a/serlib/ser_genredexpr.ml b/serlib/ser_genredexpr.ml
@@ -53,10 +53,6 @@ type ('a,'b,'c,'d) red_expr_gen =
   [%import: ('a,'b,'c,'d) Genredexpr.red_expr_gen]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('a,'b,'c,'d) may_eval =
-  [%import: ('a,'b,'c,'d) Genredexpr.may_eval]
-  [@@deriving sexp,yojson,hash,compare]
-
 (* Helpers for raw_red_expr *)
 type r_trm =
   [%import: Genredexpr.r_trm]

diff --git a/serlib/ser_genredexpr.mli b/serlib/ser_genredexpr.mli
@@ -25,9 +25,6 @@ type 'a glob_red_flag =  'a Genredexpr.glob_red_flag
 type ('a, 'b, 'c, 'd) red_expr_gen =  ('a, 'b, 'c, 'd) Genredexpr.red_expr_gen
   [@@deriving sexp,yojson,hash,compare]
 
-type ('a, 'b, 'c, 'd) may_eval =  ('a, 'b, 'c, 'd) Genredexpr.may_eval
-  [@@deriving sexp,yojson,hash,compare]
-
 type raw_red_expr = Genredexpr.raw_red_expr [@@deriving sexp,yojson,hash,compare]
 
 type 'a and_short_name = 'a Genredexpr.and_short_name