diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 22:37:33 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-23 16:53:53 +0100 |
| commit | d31056ec924ef6e09b28bc3822b427b67a8a300b (patch) | |
| tree | d720333732d9be1a03f74cc079e0a1903d31e023 /plugins/funind/recdef.ml | |
| parent | c37e90b67c74b32837409a9a424757246067ef1b (diff) | |
[vernac] Unify declaration hooks.
Supersedes #8718.
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a8517e9ab1..8746c37309 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1310,7 +1310,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); - let hook _ _ = + let hook _ _ _ _ = let opacity = let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in @@ -1560,7 +1560,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook _ _ = + let hook _ _ _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in |