diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-06 10:00:50 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-06 10:00:50 +0200 |
| commit | 24f5b8cf170012d43c00d5340173463438905ad2 (patch) | |
| tree | 7a63d3f4bfa8760561ef9db6b4e367b0d93704f5 /tactics | |
| parent | b770451a4b3c74db78457951f75505b53d362c12 (diff) | |
Make tclEFFECTS also update the env in the proof monad
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5b329a3fa..cc95430f5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4107,8 +4107,6 @@ let abstract_subproof id gk tac = let solve = Proofview.V82.tclEVARS evd <*> Proofview.tclEFFECTS effs <*> - (** Hack around *) - Proofview.tclUPDATE_ENV (Global.env ()) <*> new_exact_no_check (applist (lem, args)) in if not safe then Proofview.mark_as_unsafe <*> solve else solve |