diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 50 | ||||
| -rw-r--r-- | plugins/derive/derive.mli | 2 | ||||
| -rw-r--r-- | plugins/derive/g_derive.mlg | 6 |
3 files changed, 27 insertions, 31 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 480819ebe1..4425e41652 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -9,6 +9,7 @@ (************************************************************************) 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) @@ -27,32 +28,32 @@ let start_deriving f suchthat lemma = let sigma = Evd.from_env env in let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in - (** create a sort variable for the type of [f] *) + (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one that looked the most general. *) let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in let f_type_type = EConstr.mkSort f_type_sort in - (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) + (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in - let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in + let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in - (** The terminator handles the registering of constants when the proof is closed. *) + (* 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] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) + (* 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] + and [lemma_def] correspond to the proof of [f] and of + [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") @@ -64,26 +65,26 @@ let start_deriving f suchthat lemma = opaque <> Proof_global.Transparent , f_def , lemma_def | _ -> assert false in - (** The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) + (* The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) let f_def = { f_def with Entries.const_entry_opaque = false } in let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in let f_kn_term = mkConst f_kn in - (** In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) let substf c = Vars.replace_vars [f,f_kn_term] c in - (** Extracts the type of the proof of [suchthat]. *) + (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = match Entries.(lemma_def.const_entry_type) with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in - (** The references of [f] are subsituted appropriately. *) + (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in - (** The same is done in the body of the proof. *) + (* The same is done in the body of the proof. *) let lemma_body = map_const_entry_body substf Entries.(lemma_def.const_entry_body) in @@ -100,12 +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 18316bf2cd..214a9d8bb5 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 _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) } 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 |