Adapt to coq/coq#18546.

serlib/plugins/ltac/ser_tacexpr.ml

@@ -49,6 +49,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]
@@ -509,7 +510,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
@@ -520,7 +521,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
@@ -531,7 +532,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
@@ -542,7 +543,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
@@ -555,7 +556,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
@@ -566,7 +567,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
@@ -577,7 +578,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
@@ -588,7 +589,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
@@ -600,7 +601,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
@@ -611,7 +612,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
@@ -626,7 +627,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
@@ -637,7 +638,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
@@ -798,7 +799,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
@@ -809,7 +810,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

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]

serlib/ser_genredexpr.ml

@@ -27,6 +27,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]
@@ -101,13 +102,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

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]

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]