diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index a383b1452..9edf6302d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -785,5 +785,5 @@ END;; VERNAC COMMAND EXTEND GrabEvars [ "Grab" "Existential" "Variables" ] => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ] - -> [ Proof_global.with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] + -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] END |