diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 7b3797119a..86aa046586 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -26,7 +26,6 @@ open Libnames open Smartlocate open Termops open Inductiveops -open Typing open Typeclasses open Pattern open Patternops @@ -206,7 +205,6 @@ let write_warn_hint = function let () = Goptions.(declare_string_option { optdepr = false; - optname = "behavior of non-imported hints"; optkey = ["Loose"; "Hint"; "Behavior"]; optread = read_warn_hint; optwrite = write_warn_hint; @@ -966,16 +964,17 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (unsafe_type_of env sigma c) in + let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in let hd = head_constr sigma t in let ce = mk_clenv_from_env env sigma None (c,t) in - (Some hd, { pri=1; - poly = poly; - pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); - name = name; - db = None; - secvars = secvars_of_constr env sigma c; - code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) + (Some hd, + { pri=1; + poly = poly; + pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); + name = name; + db = None; + secvars = secvars_of_constr env sigma c; + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) |