diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 30 | ||||
| -rw-r--r-- | plugins/derive/derive.mli | 6 | ||||
| -rw-r--r-- | plugins/derive/g_derive.mlg | 4 |
3 files changed, 21 insertions, 19 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 9c1882dc9a..aad3967f6d 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -12,8 +12,8 @@ open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) - : Safe_typing.private_constants Entries.const_entry_body = +let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body) + : Evd.side_effects Entries.const_entry_body = Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end @@ -22,11 +22,11 @@ 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 - let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in + let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one @@ -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.Internal.make_terminator terminator in + let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + Lemmas.pf_map (Proof_global.map_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..de3fb9f11f 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,11 +18,11 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } 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 |