diff options
Diffstat (limited to 'vernac/comHints.ml')
| -rw-r--r-- | vernac/comHints.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/vernac/comHints.ml b/vernac/comHints.ml index 051560fb63..9eac558908 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -62,7 +62,7 @@ let project_hint ~poly pri l2r r = cb in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info, false, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c)) + (info, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c)) let warn_deprecated_hint_constr = CWarnings.create ~name:"fragile-hint-constr" ~category:"automation" @@ -89,10 +89,10 @@ let interp_hints ~poly h = let env = Global.env () in let sigma = Evd.from_env env in let c, diff = Hints.prepare_hint true env sigma (evd, c) in - if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"]) + if poly then (Hints.IsConstr (c, Some diff) [@ocaml.warning "-3"]) else let () = DeclareUctx.declare_universe_context ~poly:false diff in - (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"]) + (Hints.IsConstr (c, None) [@ocaml.warning "-3"]) in let fref r = let gr = Smartlocate.global_with_alias r in @@ -106,20 +106,20 @@ let interp_hints ~poly h = match c with | HintsReference c -> let gr = Smartlocate.global_with_alias c in - (PathHints [gr], poly, IsGlobRef gr) + (PathHints [gr], IsGlobRef gr) | HintsConstr c -> let () = warn_deprecated_hint_constr () in - (PathAny, poly, f poly c) + (PathAny, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = - let path, poly, gr = fi r in + let path, gr = fi r in let info = { info with Typeclasses.hint_pattern = Option.map fp info.Typeclasses.hint_pattern } in - (info, poly, b, path, gr) + (info, b, path, gr) in let open Hints in let open Vernacexpr in @@ -140,7 +140,6 @@ let interp_hints ~poly h = | HintsConstructors lqid -> let constr_hints_of_ind qid = let ind = Smartlocate.global_inductive_with_alias qid in - let mib, _ = Global.lookup_inductive ind in Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (Libnames.string_of_qualid qid) "ind"; @@ -148,7 +147,6 @@ let interp_hints ~poly h = let c = (ind, i + 1) in let gr = GlobRef.ConstructRef c in ( empty_hint_info - , Declareops.inductive_is_polymorphic mib , true , PathHints [gr] , IsGlobRef gr )) |