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 /proofs/proofview.mli | |
| parent | 6b0c471723a657048e50c94ea56387d54ef6eff6 (diff) | |
Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."
This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.
Conflicts:
proofs/proofview.ml
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index b1466fcfb..f59ad0dc1 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -243,16 +243,11 @@ val tclPROGRESS : 'a tactic -> 'a tactic val tclEVARMAP : Evd.evar_map tactic (* [tclENV] doesn't affect the proof, it returns the current - environment. It can be the global context or, in the context of a - {!Proofview.Goal.enter}, the context of the goal. In the latter - case, the context is the same as the environment returned by - {!Proofview.Goal.env} on the enclosing goal. *) + environment. It is not the environment of a particular goal, + rather the "global" environment of the proof. The goal-wise + environment is returned by {!Proofview.Goal.env}. *) val tclENV : Environ.env tactic -(* [tclIN_ENV e t] is the same as tactic [t] except that the global - environment it observes (obtained by {!tclENV}) is [e]. *) -val tclIN_ENV : Environ.env -> 'a tactic -> 'a tactic - (* [tclEFFECTS eff] add the effects [eff] to the current state. *) val tclEFFECTS : Declareops.side_effects -> unit tactic |