4 files changed, 18 insertions, 28 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 49c547a979..bd1f925486 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -90,7 +90,6 @@ let tac2def_typ = Entry.create "tactic:tac2def_typ"
 let tac2def_ext = Entry.create "tactic:tac2def_ext"
 let tac2def_syn = Entry.create "tactic:tac2def_syn"
 let tac2def_mut = Entry.create "tactic:tac2def_mut"
-let tac2def_run = Entry.create "tactic:tac2def_run"
 let tac2mode = Entry.create "vernac:ltac2_command"
 
 let ltac1_expr = Pltac.tactic_expr
@@ -114,7 +113,7 @@ let pattern_of_qualid qid =
 
 GRAMMAR EXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
-          tac2def_mut tac2def_run;
+          tac2def_mut;
   tac2pat:
     [ "1" LEFTA
       [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> {
@@ -288,9 +287,6 @@ GRAMMAR EXTEND Gram
   tac2def_mut:
     [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ]
   ;
-  tac2def_run:
-    [ [ "Eval"; e = tac2expr -> { StrRun e } ] ]
-  ;
   tac2typ_knd:
     [ [ t = tac2type -> { CTydDef (Some t) }
       | "["; ".."; "]" -> { CTydOpn }
@@ -878,20 +874,27 @@ PRINTED BY { pr_ltac2entry }
 | [ tac2def_ext(e) ] -> { e }
 | [ tac2def_syn(e) ] -> { e }
 | [ tac2def_mut(e) ] -> { e }
-| [ tac2def_run(e) ] -> { e }
+END
+
+VERNAC ARGUMENT EXTEND ltac2_expr
+PRINTED BY { pr_ltac2expr }
+| [ tac2expr(e) ] -> { e }
 END
 
 {
 
 let classify_ltac2 = function
 | StrSyn _ -> Vernacextend.(VtSideff [], VtNow)
-| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ | StrRun _ -> Vernacextend.classify_as_sideeff
+| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ -> Vernacextend.classify_as_sideeff
 
 }
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
-  fun ~pstate -> Tac2entries.register_struct ?local ~pstate:(Option.map Proof_global.get_current_pstate pstate) e; pstate
+| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+  Tac2entries.register_struct ?local e
+  }
+| ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> {
+  fun ~pstate -> Tac2entries.perform_eval ~pstate e
   }
 END
 
@@ -899,15 +902,6 @@ END
 
 let _ = Pvernac.register_proof_mode "Ltac2" tac2mode
 
-}
-
-VERNAC ARGUMENT EXTEND ltac2_expr
-PRINTED BY { pr_ltac2expr }
-| [ tac2expr(e) ] -> { e }
-END
-
-{
-
 open G_ltac
 open Vernacextend
 
@@ -917,9 +911,7 @@ VERNAC { tac2mode } EXTEND VernacLtac2
 | ![proof] [ ltac2_expr(t) ltac_use_default(default) ] =>
     { classify_as_proofstep } -> {
 (*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
-  fun ~pstate ->
-    Option.map (fun pstate -> Tac2entries.call ~pstate ~default t) pstate
-  }
+  fun ~pstate -> Tac2entries.call ~pstate ~default t }
 END
 
 {
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 254c2e5086..246fe47c4a 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -769,13 +769,12 @@ let perform_eval ~pstate e =
 
 (** Toplevel entries *)
 
-let register_struct ?local ~pstate str = match str with
+let register_struct ?local str = match str with
 | StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
 | StrTyp (isrec, t) -> register_type ?local isrec t
 | StrPrm (id, t, ml) -> register_primitive ?local id t ml
 | StrSyn (tok, lev, e) -> register_notation ?local tok lev e
 | StrMut (qid, e) -> register_redefinition ?local qid e
-| StrRun e -> perform_eval ~pstate e
 
 (** Toplevel exception *)
 
@@ -857,7 +856,7 @@ let print_ltac qid =
 (** Calling tactics *)
 
 let solve ~pstate default tac =
-  let pstate, status = Proof_global.with_current_proof begin fun etac p ->
+  let pstate, status = Proof_global.with_proof begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
     let g = Goal_select.get_default_goal_selector () in
     let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index e02c126e71..273cf02c9b 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -23,13 +23,14 @@ val register_primitive : ?local:bool ->
 
 val register_struct
   :  ?local:bool
-  -> pstate:Proof_global.pstate option
   -> strexpr
   -> unit
 
 val register_notation : ?local:bool -> sexpr list -> int option ->
   raw_tacexpr -> unit
 
+val perform_eval : pstate:Proof_global.pstate option -> raw_tacexpr -> unit
+
 (** {5 Notations} *)
 
 type scope_rule =
@@ -50,7 +51,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
+val call : pstate:Proof_global.pstate -> default:bool -> raw_tacexpr -> Proof_global.pstate
 
 (** {5 Toplevel exceptions} *)
 
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index 2e7dfc42db..af7bc32785 100644
--- a/user-contrib/Ltac2/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
@@ -168,8 +168,6 @@ type strexpr =
   (** Syntactic extensions *)
 | StrMut of qualid * raw_tacexpr
   (** Redefinition of mutable globals *)
-| StrRun of raw_tacexpr
-  (** Toplevel evaluation of an expression *)
 
 (** {5 Dynamic semantics} *)