Merge pull request coq/ltac2#109 from ejgallego/proof+no_global_partial

[coq] Adapt to coq/coq#9129 "removal of imperative proof state"

5 files changed, 32 insertions, 22 deletions

diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg
index 7b058a339a..a404227d3d 100644
--- a/src/g_ltac2.mlg
+++ b/src/g_ltac2.mlg
@@ -890,8 +890,8 @@ let classify_ltac2 = function
 }
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
-    Tac2entries.register_struct ?local e
+| #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+  fun ~pstate -> Tac2entries.register_struct ?local ~pstate e; pstate
   }
 END
 
@@ -914,10 +914,11 @@ open Vernacextend
 }
 
 VERNAC { tac2mode } EXTEND VernacLtac2
-| [ ltac2_expr(t) ltac_use_default(default) ] =>
+| ![proof] [ ltac2_expr(t) ltac_use_default(default) ] =>
     { classify_as_proofstep } -> {
 (*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
-    Tac2entries.call ~default t
+  fun ~pstate ->
+    Option.map (fun pstate -> Tac2entries.call ~pstate ~default t) pstate
   }
 END
 
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 15fd625650..30beee58de 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -979,6 +979,7 @@ let constr_flags () =
     fail_evar = true;
     expand_evars = true;
     program_mode = false;
+    polymorphic = false;
   }
 
 let open_constr_no_classes_flags () =
@@ -989,6 +990,7 @@ let open_constr_no_classes_flags () =
   fail_evar = false;
   expand_evars = true;
   program_mode = false;
+  polymorphic = false;
   }
 
 (** Embed all Ltac2 data into Values *)
@@ -1164,17 +1166,17 @@ let () =
 (** Ltac2 in terms *)
 
 let () =
-  let interp ist env sigma concl tac =
+  let interp ist poly env sigma concl tac =
     let ist = Tac2interp.get_env ist in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
-    let name, poly = Id.of_string "ltac2", false in
+    let name, poly = Id.of_string "ltac2", poly in
     let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2 interp
 
 let () =
-  let interp ist env sigma concl id =
+  let interp ist poly env sigma concl id =
     let ist = Tac2interp.get_env ist in
     let c = Id.Map.find id ist.env_ist in
     let c = Value.to_constr c in
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index b7ce363957..3073aad84f 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -739,19 +739,20 @@ let register_redefinition ?(local = false) qid e =
   } in
   Lib.add_anonymous_leaf (inTac2Redefinition def)
 
-let perform_eval e =
+let perform_eval ~pstate e =
   let open Proofview.Notations in
   let env = Global.env () in
   let (e, ty) = Tac2intern.intern ~strict:false e in
   let v = Tac2interp.interp Tac2interp.empty_environment e in
   let selector, proof =
-    try
-      Goal_select.get_default_goal_selector (),
-      Proof_global.give_me_the_proof ()
-    with Proof_global.NoCurrentProof ->
+    match pstate with
+    | None ->
       let sigma = Evd.from_env env in
       let name, poly = Id.of_string "ltac2", false in
       Goal_select.SelectAll, Proof.start ~name ~poly sigma []
+    | Some pstate ->
+      Goal_select.get_default_goal_selector (),
+      Proof_global.give_me_the_proof pstate
   in
   let v = match selector with
   | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
@@ -773,13 +774,13 @@ let perform_eval e =
 
 (** Toplevel entries *)
 
-let register_struct ?local str = match str with
+let register_struct ?local ~pstate 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 e
+| StrRun e -> perform_eval ~pstate e
 
 (** Toplevel exception *)
 
@@ -860,8 +861,8 @@ let print_ltac qid =
 
 (** Calling tactics *)
 
-let solve default tac =
-  let status = Proof_global.with_current_proof begin fun etac p ->
+let solve ~pstate default tac =
+  let pstate, status = Proof_global.with_current_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
@@ -869,15 +870,16 @@ let solve default tac =
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus Vernacentries.command_focus p in
     p, status
-  end in
-  if not status then Feedback.feedback Feedback.AddedAxiom
+  end pstate in
+  if not status then Feedback.feedback Feedback.AddedAxiom;
+  pstate
 
-let call ~default e =
+let call ~pstate ~default e =
   let loc = e.loc in
   let (e, t) = intern ~strict:false e in
   let () = check_unit ?loc t in
   let tac = Tac2interp.interp Tac2interp.empty_environment e in
-  solve default (Proofview.tclIGNORE tac)
+  solve ~pstate default (Proofview.tclIGNORE tac)
 
 (** Primitive algebraic types than can't be defined Coq-side *)
 
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index f97e35fec0..28b2120537 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -21,7 +21,11 @@ val register_type : ?local:bool -> rec_flag ->
 val register_primitive : ?local:bool ->
   Names.lident -> raw_typexpr -> ml_tactic_name -> unit
 
-val register_struct : ?local:bool -> strexpr -> unit
+val register_struct
+  :  ?local:bool
+  -> pstate:Proof_global.t option
+  -> strexpr
+  -> unit
 
 val register_notation : ?local:bool -> sexpr list -> int option ->
   raw_tacexpr -> unit
@@ -46,7 +50,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : default:bool -> raw_tacexpr -> unit
+val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
 
 (** {5 Toplevel exceptions} *)
 
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 059a1babd7..0c8522f495 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -24,6 +24,7 @@ let tactic_infer_flags with_evar = {
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true;
   Pretyping.program_mode = false;
+  Pretyping.polymorphic = false;
 }
 
 (** FIXME: export a better interface in Tactics *)