diff options
Diffstat (limited to 'plugins/interface/centaur.ml4')
| -rw-r--r-- | plugins/interface/centaur.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4 index e7084fbb00..07f32b6d43 100644 --- a/plugins/interface/centaur.ml4 +++ b/plugins/interface/centaur.ml4 @@ -416,7 +416,7 @@ let inspect n = | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_path sp)) (Pretyping.Default.understand Evd.empty (Global.env()) - (RRef(dummy_loc, IndRef(kn,0)))) + (RRef(dummy_loc, IndRef((mind_of_kn kn),0)))) | _ -> failwith ("unexpected value 1 for "^ (string_of_id (basename (fst oname))))) | _ -> failwith "unexpected value") |