diff options
Diffstat (limited to 'vernac/comHints.ml')
| -rw-r--r-- | vernac/comHints.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/vernac/comHints.ml b/vernac/comHints.ml index 9eac558908..b5e53208ca 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -85,14 +85,12 @@ let interp_hints ~poly h = let env = Global.env () in let sigma = Evd.from_env env in let f poly c = - let evd, c = Constrintern.interp_open_constr env sigma c in 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, Some diff) [@ocaml.warning "-3"]) - else - let () = DeclareUctx.declare_universe_context ~poly:false diff in - (Hints.IsConstr (c, None) [@ocaml.warning "-3"]) + let evd, c = Constrintern.interp_open_constr env sigma c in + let h, diff = Hints.hint_constr env sigma ~poly (evd, c) in + let () = DeclareUctx.declare_universe_context ~poly:false diff [@ocaml.warning "-3"] in + h in let fref r = let gr = Smartlocate.global_with_alias r in |