diff options
| author | Pierre-Marie Pédrot | 2020-07-17 12:01:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | 2a62e99b7fd73f58269527a1b646fae1b25570d5 (patch) | |
| tree | 90e4318d1822cb94246ba0abb8e4bef98aa3be29 /tactics/auto.ml | |
| parent | 70b7aabfdfecfc94fd5cbfd2fbf7b65cfaacdd63 (diff) | |
Split the uses of connect_hint_clenv into two different functions.
The first one is encapsulating the clenv part, and is now purely internal,
while the other one provides an abstract interfact to get fresh term instances
from a hint.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 1ba35e9113..0931c3e61e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -15,7 +15,6 @@ open Termops open Environ open Genredexpr open Tactics -open Clenv open Locus open Proofview.Notations open Hints @@ -78,10 +77,10 @@ let unify_resolve_gen = function let exact h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (exact_check c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> exact_check c end (* Util *) |