diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 55bf5f29e..c41f88ab7 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -761,7 +761,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = code = with_uid (Give_exact (c, cty, ctx)); }) let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) = - let cty = if hnf then hnf_constr env sigma cty else cty in + let cty = if hnf then hnf_constr env sigma (EConstr.of_constr cty) else cty in match kind_of_term cty with | Prod _ -> let sigma' = Evd.merge_context_set univ_flexible sigma ctx in @@ -910,7 +910,7 @@ 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 (EConstr.of_constr (unsafe_type_of env sigma c)) in let hd = head_of_constr_reference (head_constr sigma t) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; |