diff options
| author | Maxime Dénès | 2019-02-26 10:19:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-26 10:19:18 +0100 |
| commit | 3459155e1c629a2f932c4d4d917b0f69aa89ccf7 (patch) | |
| tree | 8f1db2c3e2a0d89a412c9c19b6ca458160f4c6c4 /plugins/funind/recdef.ml | |
| parent | fc76c77ac6e509c1bccc2823ce2037d21a53276a (diff) | |
| parent | d31056ec924ef6e09b28bc3822b427b67a8a300b (diff) | |
Merge PR #9567: [vernac] Unify declaration hooks.
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: maximedenes
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 |