diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-10-27 13:19:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-10-27 13:19:12 +0100 |
| commit | a57c1dc84293c5074b30d8b071a736274ab8dde8 (patch) | |
| tree | ae7b34dc469bcccdb68d2e245da0d579ff582465 | |
| parent | 35b87512d3116776d273826f3afd3646fee84594 (diff) | |
Removing the last Evd.diff from Hints.
| -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 780451e11..76cc458a6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -981,8 +981,8 @@ let prepare_hint check env init (sigma,c) = mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in let c' = iter c in if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c'; - let diff = Evd.diff sigma init in - IsConstr (c', Evd.universe_context_set diff) + let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in + IsConstr (c', diff) let interp_hints poly = fun h -> |