diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index b3c1623e0..aa1a489c2 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -36,7 +36,7 @@ let check_evars env evm = | Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_,_,false) -> () | _ -> - Pretype_errors.error_unsolvable_implicit loc env evm key None) + Pretype_errors.error_unsolvable_implicit ~loc env evm key None) (Evd.undefined_map evm) type oblinfo = @@ -260,7 +260,7 @@ let safe_init_constant md name () = Coqlib.gen_constant "Obligations" md name let hide_obligation = safe_init_constant tactics_module "obligation" -let pperror cmd = CErrors.errorlabstrm "Program" cmd +let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) let reduce c = @@ -400,7 +400,7 @@ let rec prod_app t n = | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> - errorlabstrm "prod_app" + user_err ~hdr:"prod_app" (str"Needed a product, but didn't find one" ++ fnl ()) @@ -446,7 +446,7 @@ let from_prg : program_info ProgMap.t ref = let close sec = if not (ProgMap.is_empty !from_prg) then let keys = map_keys !from_prg in - errorlabstrm "Program" + user_err ~hdr:"Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ @@ -720,7 +720,7 @@ let get_prog name = let progs = Id.Set.elements (ProgMap.domain prg_infos) in let prog = List.hd progs in let progs = prlist_with_sep pr_comma Nameops.pr_id progs in - errorlabstrm "" + user_err (str "More than one program with unsolved obligations: " ++ progs ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\"")) @@ -987,7 +987,7 @@ and solve_obligation_by_tac prg obls i tac = let (e, _) = CErrors.push e in match e with | Refiner.FailError (_, s) -> - user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) + user_err ~loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s) | e -> None (* FIXME really ? *) and solve_prg_obligations prg ?oblset tac = |