From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- pretyping/indrec.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/indrec.ml') diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 0061d8ae9..9cf91a947 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -55,7 +55,7 @@ let is_private mib = let check_privacy_block mib = if is_private mib then - user_err ""(str"case analysis on a private inductive type") + user_err (str"case analysis on a private inductive type") (**********************************************************************) (* Building case analysis schemes *) @@ -594,7 +594,7 @@ let lookup_eliminator ind_sp s = (* using short name (e.g. for "eq_rec") *) try Nametab.locate (qualid_of_ident id) with Not_found -> - user_err "default_elim" + user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ pr_id id ++ strbrk ", the elimination of the inductive definition " ++ pr_global_env Id.Set.empty (IndRef ind_sp) ++ -- cgit v1.2.3