diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-30 18:30:03 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:12 +0200 |
| commit | 2dc998e153922fffa907342871917963ad421e45 (patch) | |
| tree | a65f46be367f746e88f2d35387c3d8eead9fa13e /tactics/hints.ml | |
| parent | 4b51494ef6fee2301766fb4a44020dc2ad95799f (diff) | |
Univs: fix evar_map handling in Hint processing.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 48b450532..a7eae667d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1085,8 +1085,10 @@ let prepare_hint check env init (sigma,c) = let interp_hints poly = fun h -> + let env = (Global.env()) in + let sigma = Evd.from_env env in let f c = - let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in + let evd,c = Constrintern.interp_open_constr env sigma c in prepare_hint true (Global.env()) Evd.empty (evd,c) in let fref r = let gr = global_with_alias r in |