diff options
| author | Emilio Jesus Gallego Arias | 2016-08-19 01:58:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-08-19 02:01:56 +0200 |
| commit | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (patch) | |
| tree | caf22d0e607ed9e0bf9ba64d76b4c2aebce63d5a /ltac | |
| parent | de038270f72214b169d056642eb7144a79e6f126 (diff) | |
Remove errorlabstrm in favor of user_err
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 4 | ||||
| -rw-r--r-- | ltac/tacenv.ml | 2 | ||||
| -rw-r--r-- | ltac/tacintern.ml | 2 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 4 |
4 files changed, 6 insertions, 6 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 47c78ae5c2..e0583370ab 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1508,7 +1508,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul Evar.Set.fold (fun ev acc -> if not (Evd.is_defined acc ev) then - errorlabstrm "rewrite" + user_err "rewrite" (str "Unsolved constraint remaining: " ++ spc () ++ Evd.pr_evar_info (Evd.find acc ev)) else Evd.remove acc ev) @@ -1647,7 +1647,7 @@ let cl_rewrite_clause_strat progress strat clause = (fun gl -> try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl with RewriteFailure e -> - errorlabstrm "" (str"setoid rewrite failed: " ++ e) + user_err "" (str"setoid rewrite failed: " ++ e) | Refiner.FailError (n, pp) -> tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)) diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index c709ab114e..5808feeba3 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = let () = if Array.length tacs <= i then raise Not_found in tacs.(i) with Not_found -> - CErrors.errorlabstrm "" + CErrors.user_err "" (str "The tactic " ++ pr_tacname s ++ str " is not installed.") (***************************************************************************) diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index dc216da114..a1d34b53fa 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -748,7 +748,7 @@ let print_ltac id = ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined with Not_found -> - errorlabstrm "print_ltac" + user_err "print_ltac" (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") (** Registering *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 76c46ea7c4..b1f554eaa9 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -168,7 +168,7 @@ module Value = struct let pr_v = Pptactic.pr_value Pptactic.ltop v in let Val.Dyn (tag, _) = v in let tag = Val.pr tag in - errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag + user_err "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag ++ str " while type " ++ Val.pr wit ++ str " was expected.") let unbox wit v ans = match ans with @@ -1870,7 +1870,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma, c) = interp_constr ist env sigma c in Sigma.Unsafe.of_pair (c, sigma) with e when to_catch e (* Hack *) -> - errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") + user_err "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") end } in Tactics.change (Some op) c_interp (interp_clause ist env sigma cl) end } |