diff options
| author | Pierre-Marie Pédrot | 2014-09-04 12:16:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 12:57:33 +0200 |
| commit | 075c099b1777eea32c3a392cc039723c15c5b66e (patch) | |
| tree | a84fa7a12e40759c3fddda51517605f9c879cd7e /proofs | |
| parent | fc7a66d58c39e3d57e509c754fb4cefa96ecd488 (diff) | |
Using goal-tactics to interpret arguments to idtac.
This allows to write a multigoal idtac without having to resort to
the hack of modifying the global environment tactic through tclIN_ENV,
which may cause trouble if we want to modify it in a state-passing style.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 2c104ea181..f10843e7ae 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -857,7 +857,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let (gl, sigma) = Goal.eval enter_t env sigma goal in - tclTHEN (V82.tclEVARS sigma) ((Proof.set_local gl.env) (f gl)) + tclTHEN (V82.tclEVARS sigma) (f gl) with e when catchable_exception e -> let e = Errors.push e in tclZERO e |