diff options
| author | Maxime Dénès | 2018-03-04 16:50:36 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:50:36 +0100 |
| commit | b3a8761790c0905aad8e5d3102fab606fe5e7fd6 (patch) | |
| tree | ce5fbe8cb717bad677ad755e7875413d3e5d0e84 /tactics/hints.ml | |
| parent | 9cd987a07d3792dc200e15c5e792a25a1a99c9c6 (diff) | |
| parent | 886a9c2fb25e32bd87b3fce38023b3e701134d23 (diff) | |
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 7f9b5ef34e..10cd7e1f64 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1270,7 +1270,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let interp_hints poly = fun h -> - let env = (Global.env()) in + let env = Global.env () in let sigma = Evd.from_env env in let f poly c = let evd,c = Constrintern.interp_open_constr env sigma c in @@ -1279,9 +1279,7 @@ let interp_hints poly = let gr = global_with_alias r in Dumpglob.add_glob ?loc:(loc_of_reference r) gr; gr in - let fr r = - evaluable_of_global_reference (Global.env()) (fref r) - in + let fr r = evaluable_of_global_reference env (fref r) in let fi c = match c with | HintsReference c -> @@ -1289,7 +1287,7 @@ let interp_hints poly = (PathHints [gr], poly, IsGlobRef gr) | HintsConstr c -> (PathAny, poly, f poly c) in - let fp = Constrintern.intern_constr_pattern (Global.env()) in + let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = let path, poly, gr = fi r in let info = { info with hint_pattern = Option.map fp info.hint_pattern } in |