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/invfun.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'plugins/funind/invfun.ml')

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