From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 May 2019 19:46:02 +0200
Subject: Proof_global: pass only 1 pstate when we don't want the proof stack

Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.

Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).

We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.

Behaviour should be similar modulo bugs, let's see what CI says.
---
 plugins/derive/derive.ml    | 4 ++--
 plugins/derive/derive.mli   | 2 +-
 plugins/derive/g_derive.mlg | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 4769c2dc53..9c1882dc9a 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -101,8 +101,8 @@ let start_deriving f suchthat lemma =
       in
 
   let terminator = Proof_global.make_terminator terminator in
-  let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in
-  Proof_global.simple_with_current_proof begin fun _ p ->
+  let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in
+  Proof_global.modify_proof begin fun p ->
     let p,_,() =  Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
     p
   end pstate
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 6bb923118e..6e4bffa0b6 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 -> Proof_global.t
+val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 214a9d8bb5..ee076f5ae3 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
 | ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
-  { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) }
+  { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) }
 END
-- 
cgit v1.2.3