diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 12:12:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 12:57:33 +0200 |
| commit | fc7a66d58c39e3d57e509c754fb4cefa96ecd488 (patch) | |
| tree | 43c6a5d626b4ba182723998d31ffbe99c38d114a /tactics/tacinterp.ml | |
| parent | 6b0c471723a657048e50c94ea56387d54ef6eff6 (diff) | |
Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."
This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.
Conflicts:
proofs/proofview.ml
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f241b6373..b35955e24 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1034,23 +1034,11 @@ struct let enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> - (* the global environment of the tactic is changed to that of - the goal *) - Proofview.tclIN_ENV (Proofview.Goal.env gl) ( - Proofview.V82.wrap_exceptions (fun () -> f gl) - ) - ) + (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let raw_enter f = bind (Proofview.Goal.raw_goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> - (* the global environment of the tactic is changed to that of - the goal *) - Proofview.tclIN_ENV (Proofview.Goal.env gl) ( - Proofview.V82.wrap_exceptions (fun () -> f gl) - ) - ) + (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let lift (type a) (t:a Proofview.tactic) : a t = Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) |