Merge pull request #360 from SkySkimmer/redexpr

Adapt to coq/coq#17503 (raw/glob_red_expr moved)
rocq-archive · Oct 25, 2023 · 3673c01 · 3673c01
2 parents e0a79cd + 7228d5c
commit 3673c01
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 34 deletions.
diff --git a/serlib/plugins/ltac/ser_tacarg.ml b/serlib/plugins/ltac/ser_tacarg.ml
@@ -32,6 +32,7 @@ module Geninterp    = Ser_geninterp
 module EConstr      = Ser_eConstr
 module Hints        = Ser_hints
 module Ltac_pretype = Ser_ltac_pretype
+module Genredexpr   = Ser_genredexpr
 
 module Ltac_plugin = struct
   module G_rewrite    = G_rewrite

diff --git a/serlib/plugins/ltac/ser_tacexpr.ml b/serlib/plugins/ltac/ser_tacexpr.ml
@@ -825,23 +825,3 @@ type tacdef_body =
 type intro_pattern =
   [%import: Ltac_plugin.Tacexpr.intro_pattern]
   [@@deriving sexp,yojson,hash,compare]
-
-type raw_red_expr =
-  [%import: Ltac_plugin.Tacexpr.raw_red_expr]
-  [@@deriving sexp,yojson,hash,compare]
-
-type g_trm =
-  [%import: Ltac_plugin.Tacexpr.g_trm]
-  [@@deriving sexp,yojson,hash,compare]
-
-type g_cst =
-  [%import: Ltac_plugin.Tacexpr.g_cst]
-  [@@deriving sexp,yojson,hash,compare]
-
-type g_pat =
-  [%import: Ltac_plugin.Tacexpr.g_pat]
-  [@@deriving sexp,yojson,hash,compare]
-
-type glob_red_expr =
-  [%import: Ltac_plugin.Tacexpr.glob_red_expr]
-  [@@deriving sexp,yojson,hash,compare]
diff --git a/serlib/plugins/ltac/ser_tacexpr.mli b/serlib/plugins/ltac/ser_tacexpr.mli
@@ -267,9 +267,3 @@ type tacdef_body = Tacexpr.tacdef_body
 
 type intro_pattern = Tacexpr.intro_pattern
   [@@deriving sexp,hash,compare]
-
-type raw_red_expr = Tacexpr.raw_red_expr
-  [@@deriving sexp,hash,compare]
-
-type glob_red_expr = Tacexpr.glob_red_expr
-  [@@deriving sexp,hash,compare]
diff --git a/serlib/ser_genredexpr.ml b/serlib/ser_genredexpr.ml
@@ -23,11 +23,17 @@ module Util  = Ser_util
 module Locus = Ser_locus
 module Libnames = Ser_libnames
 module Constrexpr = Ser_constrexpr
+module Genintern = Ser_genintern
+module Tacred = Ser_tacred
 
 type 'a red_atom =
   [%import: 'a Genredexpr.red_atom]
   [@@deriving sexp]
 
+type strength =
+  [%import: Genredexpr.strength]
+  [@@deriving sexp,yojson,hash,compare]
+
 type 'a glob_red_flag =
   [%import: 'a Genredexpr.glob_red_flag]
   [@@deriving sexp,yojson,hash,compare]
@@ -61,10 +67,28 @@ type raw_red_expr =
   [%import: Genredexpr.raw_red_expr]
   [@@deriving sexp,yojson,hash,compare]
 
+(* glob_red_expr *)
+
 type 'a and_short_name =
   [%import: 'a Genredexpr.and_short_name]
   [@@deriving sexp,yojson,hash,compare]
 
+type g_trm =
+  [%import: Genredexpr.g_trm]
+  [@@deriving sexp,yojson,hash,compare]
+
+type g_cst =
+  [%import: Genredexpr.g_cst]
+  [@@deriving sexp,yojson,hash,compare]
+
+type g_pat =
+  [%import: Genredexpr.g_pat]
+  [@@deriving sexp,yojson,hash,compare]
+
+type glob_red_expr =
+  [%import: Genredexpr.glob_red_expr]
+  [@@deriving sexp,yojson,hash,compare]
+
 module A = struct
 
   type raw =

diff --git a/serlib/ser_genredexpr.mli b/serlib/ser_genredexpr.mli
@@ -35,14 +35,8 @@ type ('a, 'b, 'c) may_eval =  ('a, 'b, 'c) Genredexpr.may_eval
 
 type raw_red_expr = Genredexpr.raw_red_expr [@@deriving sexp,yojson,hash,compare]
 
-type r_cst = Genredexpr.r_cst
-  [@@deriving sexp,yojson,hash,compare]
-
-type r_trm = Genredexpr.r_trm
-  [@@deriving sexp,yojson,hash,compare]
-
-type r_pat = Genredexpr.r_pat
+type 'a and_short_name = 'a Genredexpr.and_short_name
   [@@deriving sexp,yojson,hash,compare]
 
-type 'a and_short_name = 'a Genredexpr.and_short_name
+type glob_red_expr = Genredexpr.glob_red_expr
   [@@deriving sexp,yojson,hash,compare]