From fd7f056b155b2ebaafa3251a3c136117ebefc3e3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 29 May 2017 11:48:51 +0200
Subject: Cleanup: removal of constr_of_global.

Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.
---
 plugins/funind/merge.ml | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b2c8489ce1..7634437171 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -133,20 +133,6 @@ let prNamedRLDecl s lc =
     prstr "\n";
   end
 
-let showind (id:Id.t) =
-  let cstrid = Constrintern.global_reference id in
-  let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
-  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
-  let u = EConstr.Unsafe.to_instance u in
-  List.iter (fun decl ->
-    print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
-    prconstr (RelDecl.get_type decl); print_string "\n")
-    ib1.mind_arity_ctxt;
-    Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u));
-  Array.iteri
-    (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
-    ib1.mind_user_lc
-
 (** {2 Misc} *)
 
 exception Found of int
-- 
cgit v1.2.3