diff options
| author | Emilio Jesus Gallego Arias | 2018-12-05 01:03:51 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | 6ac4cfe51abf41c9e3bccb5f760df57258495a86 (patch) | |
| tree | fff08ba32e223fc787154c9387be8d5d0c53ae5d /plugins | |
| parent | 0e905b4934296a09115fc9cb06903ee8fcdf04bf (diff) | |
[plugins] [derive] Adapt to removal of imperative proof state.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/derive.ml | 7 | ||||
| -rw-r--r-- | plugins/derive/derive.mli | 2 | ||||
| -rw-r--r-- | plugins/derive/g_derive.mlg | 4 |
3 files changed, 6 insertions, 7 deletions
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 |