From 6ac4cfe51abf41c9e3bccb5f760df57258495a86 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 5 Dec 2018 01:03:51 +0100
Subject: [plugins] [derive] Adapt to removal of imperative proof state.

---
 plugins/derive/derive.ml    | 7 +++----
 plugins/derive/derive.mli   | 2 +-
 plugins/derive/g_derive.mlg | 4 ++--
 3 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index afdbfa1999..4425e41652 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -101,8 +101,7 @@ let start_deriving f suchthat lemma =
       in
 
   let terminator = Proof_global.make_terminator terminator in
-  let () = Proof_global.start_dependent_proof lemma kind goals terminator in
-  let _ = Proof_global.with_current_proof begin fun _ p ->
+  let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in
+  fst @@ Proof_global.with_current_proof begin fun _ p ->
     Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-  end in
-  ()
+  end pstate
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 06ff9c48cf..6bb923118e 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -12,4 +12,4 @@
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> unit
+val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 0cdf8fb5d8..214a9d8bb5 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -23,6 +23,6 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
 }
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
-| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
-  { Derive.start_deriving f suchthat lemma }
+| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
+  { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) }
 END
-- 
cgit v1.2.3