diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index eb50a2a67c..7b3797119a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1289,8 +1289,7 @@ let prepare_hint check env init (sigma,c) = mkNamedLambda (make_annot id Sorts.Relevant) t (iter (replace_term sigma evar (mkVar id) c)) in let c' = iter c in let env = Global.env () in - let empty_sigma = Evd.from_env env in - if check then Pretyping.check_evars env empty_sigma sigma c'; + if check then Pretyping.check_evars env sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in (c', diff) |