diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/Derive/derive.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml index bf4b78b048..fbf7131e67 100644 --- a/plugins/Derive/derive.ml +++ b/plugins/Derive/derive.ml @@ -55,19 +55,18 @@ let start_deriving f suchthat lemma = 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 = Term.mkConst f_kn in + let substf c = Vars.replace_vars [f,f_kn_term] c in let lemma_pretype = match Entries.(lemma_def.const_entry_type) with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in (* substitutes the variable [f] by the constant [f] it was standing for. *) - let lemma_type = Vars.replace_vars [f,f_kn_term] lemma_pretype in + let lemma_type = substf lemma_pretype in (* The type of [lemma_def] is adjusted to refer to [f_kn], the opacity is adjusted by the proof ending command. *) let lemma_body = - map_const_entry_body begin fun c -> - Vars.replace_vars [f,f_kn_term] c - end Entries.(lemma_def.const_entry_body) + map_const_entry_body substf Entries.(lemma_def.const_entry_body) in let lemma_def = let open Entries in { lemma_def with const_entry_body = lemma_body ; |