diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 2 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index a1094e39a4..bbc4df7dde 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -151,7 +151,7 @@ let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Gena Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = - Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) + Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) } diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 1ea803f561..012fcee486 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1860,13 +1860,13 @@ let do_generate_principle_aux pconstants on_error register_built let warn_cannot_define_graph = CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" (fun (names, error) -> - Pp.(strbrk "Cannot define graph(s) for " ++ h 1 names ++ error)) + Pp.(strbrk "Cannot define graph(s) for " ++ hv 1 names ++ error)) let warn_cannot_define_principle = CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" (fun (names, error) -> Pp.( - strbrk "Cannot define induction principle(s) for " ++ h 1 names ++ error)) + strbrk "Cannot define induction principle(s) for " ++ hv 1 names ++ error)) let warning_error names e = let e_explain e = @@ -1898,7 +1898,7 @@ let error_error names e = CErrors.user_err Pp.( str "Cannot define graph(s) for " - ++ h 1 + ++ hv 1 (prlist_with_sep (fun _ -> str "," ++ spc ()) Ppconstr.pr_id names) ++ e_explain e) | _ -> raise e |