aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/merge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r--plugins/funind/merge.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 865042afb..222c0c804 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -135,7 +135,7 @@ let prNamedRLDecl s lc =
let showind (id:Id.t) =
let cstrid = Constrintern.global_reference id in
- let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
+ let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
List.iter (fun decl ->
print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");