aboutsummaryrefslogtreecommitdiff
path: root/src/tac2entries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2entries.ml')
-rw-r--r--src/tac2entries.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index bba4680a72..22025f0a8f 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -750,7 +750,8 @@ let perform_eval e =
Proof_global.give_me_the_proof ()
with Proof_global.NoCurrentProof ->
let sigma = Evd.from_env env in
- Goal_select.SelectAll, Proof.start sigma []
+ let name, poly = Id.of_string "ltac2", false in
+ Goal_select.SelectAll, Proof.start ~name ~poly sigma []
in
let v = match selector with
| Goal_select.SelectNth i -> Proofview.tclFOCUS i i v