diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 24 | ||||
| -rw-r--r-- | plugins/derive/derive.mli | 6 | ||||
| -rw-r--r-- | plugins/derive/g_derive.mlg | 2 |
3 files changed, 17 insertions, 15 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 7c0f269481..fd5b3a7e48 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -22,7 +22,7 @@ let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Ent (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. *) -let start_deriving f suchthat lemma = +let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in @@ -48,7 +48,6 @@ let start_deriving f suchthat lemma = (* The terminator handles the registering of constants when the proof is closed. *) let terminator com = - let open Proof_global in (* Extracts the relevant information from the proof. [Admitted] and [Save] result in user errors. [opaque] is [true] if the proof was concluded by [Qed], and [false] if [Defined]. [f_def] @@ -56,10 +55,10 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Proved (_,Some _,_) -> + | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") + | Lemmas.Proved (_,Some _,_) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Proved (opaque, None, obj) -> + | Lemmas.Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def @@ -97,12 +96,11 @@ let start_deriving f suchthat lemma = Entries.DefinitionEntry lemma_def , Decl_kinds.(IsProof Proposition) in - ignore (Declare.declare_constant lemma lemma_def) - in + ignore (Declare.declare_constant name lemma_def) + in - let terminator = Proof_global.make_terminator terminator in - 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 + let terminator ?hook _ = Lemmas.make_terminator terminator in + let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + Lemmas.simple_with_proof begin fun _ p -> + Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + end lemma diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6bb923118e..ffbc726e22 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,8 @@ (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 + -> Lemmas.t diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 526989fdf3..6c9cd66f96 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 } STATE open_proof | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { Derive.(start_deriving f suchthat lemma) } + { Derive.start_deriving f suchthat lemma } END |