diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:35:47 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:46:38 +0200 |
commit | fc579fdc83b751a44a18d2373e86ab38806e7306 (patch) | |
tree | b325c2ff65c505ad62ac7b3fce6bce28633a60f0 /pretyping/tacred.ml | |
parent | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff) |
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r-- | pretyping/tacred.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 67819dc98..bb883b29f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -38,7 +38,7 @@ exception Elimconst exception Redelimination let error_not_evaluable r = - user_err "error_not_evaluable" + user_err ~hdr:"error_not_evaluable" (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ str "to an evaluable reference.") @@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> incr pos; if ok then begin if Option.has_some nested then - user_err "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str "."); + user_err (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str "."); (* Skip inner occurrences for stable counting of occurrences *) if locs != [] then ignore (traverse_below (Some (!pos-1)) envc t); @@ -1159,13 +1159,13 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> let check_privacy env ind = let spec = Inductive.lookup_mind_specif env (fst ind) in if Inductive.is_private spec then - user_err "" (str "case analysis on a private type.") + user_err (str "case analysis on a private type.") else ind let check_not_primitive_record env ind = let spec = Inductive.lookup_mind_specif env (fst ind) in if Inductive.is_primitive_record spec then - user_err "" (str "case analysis on a primitive record type: " ++ + user_err (str "case analysis on a primitive record type: " ++ str "use projections or let instead.") else ind @@ -1182,14 +1182,14 @@ let reduce_to_ind_gen allow_product env sigma t = if allow_product then elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else - user_err "" (str"Not an inductive definition.") + user_err (str"Not an inductive definition.") | _ -> (* Last chance: we allow to bypass the Opaque flag (as it was partially the case between V5.10 and V8.1 *) let t' = whd_all env sigma t in match kind_of_term (fst (decompose_app t')) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) - | _ -> user_err "" (str"Not an inductive product.") + | _ -> user_err (str"Not an inductive product.") in elimrec env t [] @@ -1239,7 +1239,7 @@ let one_step_reduce env sigma c = applist (redrec (c,[])) let error_cannot_recognize ref = - user_err "" + user_err (str "Cannot recognize a statement based on " ++ Nametab.pr_global_env Id.Set.empty ref ++ str".") |