Adapt to coq/coq#18546.

rocq-archive · Feb 6, 2024 · 249649c · 249649c
1 parent 4d38ca0
commit 249649c
Show file tree

Hide file tree

Showing 5 changed files with 42 additions and 25 deletions.
diff --git a/serlib/plugins/ltac/ser_tacexpr.ml b/serlib/plugins/ltac/ser_tacexpr.ml
@@ -48,6 +48,7 @@ module Tactypes   = Ser_tactypes
 module Tactics    = Ser_tactics
 module Equality   = Ser_equality
 module Inv        = Ser_inv
+module Evaluable  = Ser_evaluable
 
 type direction_flag =
   [%import: Ltac_plugin.Tacexpr.direction_flag]
@@ -508,7 +509,7 @@ let rec glob_tactic_expr_of_sexp tac =
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_pattern_and_expr_of_sexp
-    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Names.Evaluable.t_of_sexp))
+    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Evaluable.t_of_sexp))
     (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp))
     Names.lident_of_sexp
     glob_tactic_expr_of_sexp
@@ -519,7 +520,7 @@ and glob_atomic_tactic_expr_of_sexp tac =
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_and_expr_of_sexp
     Genintern.glob_constr_pattern_and_expr_of_sexp
-    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Names.Evaluable.t_of_sexp))
+    (Locus.or_var_of_sexp (Genredexpr.and_short_name_of_sexp Evaluable.t_of_sexp))
     (Locus.or_var_of_sexp (Loc.located_of_sexp ltac_constant_of_sexp))
     Names.lident_of_sexp
     glob_tactic_expr_of_sexp
@@ -530,7 +531,7 @@ let rec sexp_of_glob_tactic_expr (tac : glob_tactic_expr) =
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_pattern_and_expr
-    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Names.Evaluable.sexp_of_t))
+    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Evaluable.sexp_of_t))
     (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant))
     Names.sexp_of_lident
     sexp_of_glob_tactic_expr
@@ -541,7 +542,7 @@ and sexp_of_glob_atomic_tactic_expr (tac : glob_atomic_tactic_expr) =
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_and_expr
     Genintern.sexp_of_glob_constr_pattern_and_expr
-    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Names.Evaluable.sexp_of_t))
+    (Locus.sexp_of_or_var (Genredexpr.sexp_of_and_short_name Evaluable.sexp_of_t))
     (Locus.sexp_of_or_var (Loc.sexp_of_located sexp_of_ltac_constant))
     Names.sexp_of_lident
     sexp_of_glob_tactic_expr
@@ -554,7 +555,7 @@ let rec glob_tactic_expr_of_yojson tac =
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_pattern_and_expr_of_yojson
-    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Names.Evaluable.of_yojson))
+    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Evaluable.of_yojson))
     (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson))
     Names.lident_of_yojson
     glob_tactic_expr_of_yojson
@@ -565,7 +566,7 @@ and glob_atomic_tactic_expr_of_yojson tac =
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_and_expr_of_yojson
     Genintern.glob_constr_pattern_and_expr_of_yojson
-    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Names.Evaluable.of_yojson))
+    (Locus.or_var_of_yojson (Genredexpr.and_short_name_of_yojson Evaluable.of_yojson))
     (Locus.or_var_of_yojson (Loc.located_of_yojson ltac_constant_of_yojson))
     Names.lident_of_yojson
     glob_tactic_expr_of_yojson
@@ -576,7 +577,7 @@ let rec glob_tactic_expr_to_yojson tac =
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_pattern_and_expr_to_yojson
-    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Names.Evaluable.to_yojson))
+    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Evaluable.to_yojson))
     (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson))
     Names.lident_to_yojson
     glob_tactic_expr_to_yojson
@@ -587,7 +588,7 @@ and glob_atomic_tactic_expr_to_yojson tac =
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_and_expr_to_yojson
     Genintern.glob_constr_pattern_and_expr_to_yojson
-    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Names.Evaluable.to_yojson))
+    (Locus.or_var_to_yojson (Genredexpr.and_short_name_to_yojson Evaluable.to_yojson))
     (Locus.or_var_to_yojson (Loc.located_to_yojson ltac_constant_to_yojson))
     Names.lident_to_yojson
     glob_tactic_expr_to_yojson
@@ -599,7 +600,7 @@ let rec hash_fold_glob_tactic_expr st tac =
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_pattern_and_expr
-    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Names.Evaluable.hash_fold_t))
+    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Evaluable.hash_fold_t))
     (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant))
     Names.hash_fold_lident
     hash_fold_glob_tactic_expr
@@ -610,7 +611,7 @@ and hash_fold_glob_atomic_tactic_expr st tac =
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_and_expr
     Genintern.hash_fold_glob_constr_pattern_and_expr
-    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Names.Evaluable.hash_fold_t))
+    (Locus.hash_fold_or_var (Genredexpr.hash_fold_and_short_name Evaluable.hash_fold_t))
     (Locus.hash_fold_or_var (Loc.hash_fold_located hash_fold_ltac_constant))
     Names.hash_fold_lident
     hash_fold_glob_tactic_expr
@@ -625,7 +626,7 @@ let rec compare_glob_tactic_expr tac =
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_pattern_and_expr
-    (Locus.compare_or_var (Genredexpr.compare_and_short_name Names.Evaluable.compare))
+    (Locus.compare_or_var (Genredexpr.compare_and_short_name Evaluable.compare))
     (Locus.compare_or_var (Loc.compare_located compare_ltac_constant))
     Names.compare_lident
     compare_glob_tactic_expr
@@ -636,7 +637,7 @@ and compare_glob_atomic_tactic_expr tac =
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_and_expr
     Genintern.compare_glob_constr_pattern_and_expr
-    (Locus.compare_or_var (Genredexpr.compare_and_short_name Names.Evaluable.compare))
+    (Locus.compare_or_var (Genredexpr.compare_and_short_name Evaluable.compare))
     (Locus.compare_or_var (Loc.compare_located compare_ltac_constant))
     Names.compare_lident
     compare_glob_tactic_expr
@@ -797,7 +798,7 @@ let atomic_tactic_expr_of_sexp tac =
     EConstr.t_of_sexp
     Genintern.glob_constr_and_expr_of_sexp
     Pattern.constr_pattern_of_sexp
-    Names.Evaluable.t_of_sexp
+    Evaluable.t_of_sexp
     (Loc.located_of_sexp ltac_constant_of_sexp)
     Names.Id.t_of_sexp
     unit_of_sexp
@@ -808,7 +809,7 @@ let sexp_of_atomic_tactic_expr tac =
     EConstr.sexp_of_t
     Genintern.sexp_of_glob_constr_and_expr
     Pattern.sexp_of_constr_pattern
-    Names.Evaluable.sexp_of_t
+    Evaluable.sexp_of_t
     (Loc.sexp_of_located sexp_of_ltac_constant)
     Names.Id.sexp_of_t
     sexp_of_unit

diff --git a/serlib/ser_evaluable.ml b/serlib/ser_evaluable.ml
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq serialization API/Plugin                                         *)
+(* Copyright 2016-2019 MINES ParisTech                                  *)
+(* Copyright 2019-2021 Inria                                            *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+(* Status: Very Experimental                                            *)
+(************************************************************************)
+
+module Names = Ser_names
+
+type t =
+  [%import: Evaluable.t]
+  [@@deriving sexp,yojson,hash,compare]
diff --git a/serlib/ser_genredexpr.ml b/serlib/ser_genredexpr.ml
@@ -24,6 +24,7 @@ module Locus = Ser_locus
 module Libnames = Ser_libnames
 module Constrexpr = Ser_constrexpr
 module Genintern = Ser_genintern
+module Evaluable = Ser_evaluable
 
 type 'a red_atom =
   [%import: 'a Genredexpr.red_atom]
@@ -98,13 +99,13 @@ module A = struct
 
   type glb =
     (Ser_genintern.glob_constr_and_expr,
-     Ser_names.Evaluable.t and_short_name Ser_locus.or_var,
+     Ser_evaluable.t and_short_name Ser_locus.or_var,
      Ser_genintern.glob_constr_pattern_and_expr) red_expr_gen
   [@@deriving sexp,yojson,hash,compare]
 
   type top =
     (Ser_eConstr.constr,
-     Ser_names.Evaluable.t,
+     Ser_evaluable.t,
      Ser_pattern.constr_pattern) red_expr_gen
   [@@deriving sexp,yojson,hash,compare]
 end

diff --git a/serlib/ser_names.ml b/serlib/ser_names.ml
@@ -266,13 +266,6 @@ type t = [%import: Names.GlobRef.t]
 
 end
 
-(* Evaluable global reference: public *)
-module Evaluable = struct
-  type t =
-    [%import: Names.Evaluable.t]
-    [@@deriving sexp,yojson,hash,compare]
-end
-
 type lident =
   [%import: Names.lident]
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_names.mli b/serlib/ser_names.mli
@@ -74,8 +74,6 @@ end
 
 module GlobRef : SerType.SJHC with type t = Names.GlobRef.t
 
-module Evaluable : SerType.SJHC with type t = Names.Evaluable.t
-
 type lident = Names.lident [@@deriving sexp,yojson,hash,compare]
 type lname = Names.lname [@@deriving sexp,yojson,hash,compare]
 type lstring = Names.lstring [@@deriving sexp,yojson,hash,compare]