From ce22c1cb3bca8381d9b0ebfef2fbf27e92418b0c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 Jul 2019 15:32:57 +0200
Subject: [funind] Move common `make_eq` to funind_common.

---
 plugins/funind/gen_principle.ml  | 4 ----
 plugins/funind/indfun_common.ml  | 4 ++++
 plugins/funind/indfun_common.mli | 1 +
 plugins/funind/invfun.ml         | 5 -----
 4 files changed, 5 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index a6c5e63ecf..72975d6871 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -15,10 +15,6 @@ open Indfun_common
 
 module RelDecl = Context.Rel.Declaration
 
-let make_eq () =
-  try EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
-  with _ -> assert false
-
 (* Move to common *)
 let observe strm =
   if do_observe ()
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2d8d10a1f2..5cc3c96983 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -429,6 +429,10 @@ let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_gl
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
+let make_eq () =
+  try EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
+  with _ -> assert false
+
 let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
   match r with
       GlobRef.ConstRef sp -> EvalConstRef sp
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index a95b1242ac..0b8cbf6dc5 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -41,6 +41,7 @@ val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
+val make_eq : unit -> EConstr.constr
 
 val save
   :  Id.t
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 90631d8e55..1407585bff 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -30,11 +30,6 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 (*     raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) *)
 
 
-let make_eq () =
-  try
-    EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
-  with _ -> assert false
-
 (***********************************************)
 
 (* [revert_graph kn post_tac hid] transforme an hypothesis [hid] having type Ind(kn,num) t1 ... tn res
-- 
cgit v1.2.3