diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 681db5d08..2fc8baa89 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1306,7 +1306,8 @@ let interp_hints poly = List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - empty_hint_info, mib.Declarations.mind_polymorphic, true, + empty_hint_info, + (Declareops.inductive_is_polymorphic mib), true, PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> |