diff options
Diffstat (limited to 'plugins/derive/derive.ml')
| -rw-r--r-- | plugins/derive/derive.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index ce93c5a3..e39d17b5 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Context.Named.Declaration + let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) : Safe_typing.private_constants Entries.const_entry_body = Future.chain ~pure:true x begin fun ((b,ctx),fx) -> @@ -32,7 +34,7 @@ let start_deriving f suchthat lemma = let open Proofview in TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> - let env' = Environ.push_named (f , (Some ef) , f_type) env in + let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in let evdref = ref sigma in let suchthat = Constrintern.interp_type_evars env' evdref suchthat in TCons ( env' , !evdref , suchthat , (fun sigma _ -> @@ -49,9 +51,9 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> Errors.error"Admitted isn't supported in Derive." + | Admitted _ -> CErrors.error"Admitted isn't supported in Derive." | Proved (_,Some _,_) -> - Errors.error"Cannot save a proof of Derive with an explicit name." + CErrors.error"Cannot save a proof of Derive with an explicit name." | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> @@ -93,6 +95,7 @@ let start_deriving f suchthat lemma = ignore (Declare.declare_constant lemma lemma_def) 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 -> Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p |