aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2016-08-19 01:58:04 +0200
committerEmilio Jesus Gallego Arias2016-08-19 02:01:56 +0200
commit543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (patch)
treecaf22d0e607ed9e0bf9ba64d76b4c2aebce63d5a /tactics
parentde038270f72214b169d056642eb7144a79e6f126 (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 'tactics')
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/eauto.ml6
-rw-r--r--tactics/equality.ml10
-rw-r--r--tactics/hints.ml6
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml10
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml50
9 files changed, 46 insertions, 46 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3257d406a1..b898ceb046 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -65,7 +65,7 @@ let raw_find_base bas = String.Map.find bas !rewtab
let find_base bas =
try raw_find_base bas
with Not_found ->
- errorlabstrm "AutoRewrite"
+ user_err "AutoRewrite"
(str "Rewriting base " ++ str bas ++ str " does not exist.")
let find_rewrites bas =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2eca1e597c..dcf3dea106 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -98,7 +98,7 @@ let prolog_tac l n =
let l = List.map map l in
try (prolog l n gl)
with UserError ("Refiner.tclFIRST",_) ->
- errorlabstrm "Prolog.prolog" (str "Prolog failed.")
+ user_err "Prolog.prolog" (str "Prolog failed.")
end
open Auto
@@ -431,7 +431,7 @@ let cons a l = a :: l
let autounfolds db occs cls gl =
let unfolds = List.concat (List.map (fun dbname ->
let db = try searchtable_map dbname
- with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+ with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname)
in
let (ids, csts) = Hint_db.unfolds db in
let hyps = pf_ids_of_hyps gl in
@@ -498,7 +498,7 @@ let autounfold_one db cl =
let st =
List.fold_left (fun (i,c) dbname ->
let db = try searchtable_map dbname
- with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+ with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname)
in
let (ids, csts) = Hint_db.unfolds db in
(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2c97cf4425..4391a96b17 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -359,7 +359,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
let _ = Global.lookup_constant c1' in
c1'
with Not_found ->
- errorlabstrm "Equality.find_elim"
+ user_err "Equality.find_elim"
(str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
end
| _ -> destConstRef pr1
@@ -888,7 +888,7 @@ let build_selector env sigma dirn c ind special default =
on (c bool true) = (c bool false)
CP : changed assert false in a more informative error
*)
- errorlabstrm "Equality.construct_discriminator"
+ user_err "Equality.construct_discriminator"
(str "Cannot discriminate on inductive constructors with \
dependent types.") in
let (indp,_) = dest_ind_family indf in
@@ -974,7 +974,7 @@ let apply_on_clause (f,t) clause =
let argmv =
(match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
| Meta mv -> mv
- | _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
+ | _ -> user_err "" (str "Ill-formed clause applicator.")) in
clenv_fchain ~with_univs:false argmv f_clause clause
let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
@@ -1052,7 +1052,7 @@ let discrEverywhere with_evars =
else (* <= 8.2 compat *)
tryAllHypsAndConcl (discrSimpleClause with_evars))
(* (fun gls ->
- errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
+ user_err "DiscrEverywhere" (str"No discriminable equalities."))
*)
let discr_tac with_evars = function
| None -> discrEverywhere with_evars
@@ -1725,7 +1725,7 @@ let subst_one_var dep_proof_ok x =
let hyps = Proofview.Goal.hyps gl in
let test hyp _ = is_eq_x gl x hyp in
Context.Named.fold_outside test ~init:() hyps;
- errorlabstrm "Subst"
+ user_err "Subst"
(str "Cannot find any non-recursive equality over " ++ pr_id x ++
str".")
with FoundHyp res -> res in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8f3eb5eb51..e706316d7b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -632,7 +632,7 @@ let current_pure_db () =
List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
let error_no_such_hint_database x =
- errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
+ user_err "Hints" (str "No such Hint database: " ++ str x ++ str ".")
(**************************************************************************)
(* Definition of the summary *)
@@ -774,7 +774,7 @@ let make_resolves env sigma flags pri poly ?name cr =
[make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name]
in
if List.is_empty ents then
- errorlabstrm "Hint"
+ user_err "Hint"
(pr_lconstr c ++ spc() ++
(if pi1 flags then str"cannot be used as a hint."
else str "can be used as a hint only for eauto."));
@@ -817,7 +817,7 @@ let make_mode ref m =
let n = List.length ctx in
let m' = Array.of_list m in
if not (n == Array.length m') then
- errorlabstrm "Hint"
+ user_err "Hint"
(pr_global ref ++ str" has " ++ int n ++
str" arguments while the mode declares " ++ int (Array.length m'))
else m'
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6e24cc4698..aee3bc45d5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -450,7 +450,7 @@ let find_this_eq_data_decompose gl eqn =
try (*first_match (match_eq eqn) inversible_equalities*)
find_eq_data eqn
with PatternMatchingFailure ->
- errorlabstrm "" (str "No primitive equality found.") in
+ user_err "" (str "No primitive equality found.") in
let eq_args =
try extract_eq_args gl eq_args
with PatternMatchingFailure ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index bda16b01c0..a7f5ded5bc 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -76,7 +76,7 @@ let make_inv_predicate env evd indf realargs id status concl =
(hyps_arity,concl)
| Dep dflt_concl ->
if not (occur_var env id concl) then
- errorlabstrm "make_inv_predicate"
+ user_err "make_inv_predicate"
(str "Current goal does not depend on " ++ pr_id id ++ str".");
(* We abstract the conclusion of goal with respect to
realargs and c to * be concl in order to rewrite and have
@@ -440,7 +440,7 @@ let raw_inversion inv_kind id status names =
try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
with UserError _ ->
let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
- CErrors.errorlabstrm "" msg
+ CErrors.user_err "" msg
in
let IndType (indf,realargs) = find_rectype env sigma t in
let evdref = ref sigma in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 642bf520b1..e83093b0ce 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -183,7 +183,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let ind =
try find_rectype env sigma i
with Not_found ->
- errorlabstrm "inversion_scheme" (no_inductive_inconstr env sigma i)
+ user_err "inversion_scheme" (no_inductive_inconstr env sigma i)
in
let (invEnv,invGoal) =
compute_first_inversion_scheme env sigma ind sort dep_option
@@ -193,7 +193,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
(global_vars env invGoal)
(ids_of_named_context (named_context invEnv)));
(*
- errorlabstrm "lemma_inversion"
+ user_err "lemma_inversion"
(str"Computed inversion goal was not closed in initial signature.");
*)
let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
@@ -248,7 +248,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
add_inversion_lemma na env sigma c sort bool tac
with
| UserError ("Case analysis",s) -> (* Reference to Indrec *)
- errorlabstrm "Inv needs Nodep Prop Set" s
+ user_err "Inv needs Nodep Prop Set" s
(* ================================= *)
(* Applying a given inversion lemma *)
@@ -261,10 +261,10 @@ let lemInv id c gls =
Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
with
| NoSuchBinding ->
- errorlabstrm ""
+ user_err ""
(hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
| UserError (a,b) ->
- errorlabstrm "LemInv"
+ user_err "LemInv"
(str "Cannot refine current goal with the lemma " ++
pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 28a7b634c6..c9af1f11ca 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -643,7 +643,7 @@ module New = struct
| Var id -> string_of_id id
| _ -> "\b"
in
- errorlabstrm "Tacticals.general_elim_then_using"
+ user_err "Tacticals.general_elim_then_using"
(str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ef66e61461..16643b6a75 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -183,7 +183,7 @@ let introduction ?(check=true) id =
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
let () = if check && mem_named_context id hyps then
- errorlabstrm "Tactics.introduction"
+ user_err "Tactics.introduction"
(str "Variable " ++ pr_id id ++ str " is already declared.")
in
match kind_of_term (whd_evar sigma concl) with
@@ -255,7 +255,7 @@ let clear_dependency_msg env sigma id = function
Printer.pr_existential env sigma ev ++ str"."
let error_clear_dependency env sigma id err =
- errorlabstrm "" (clear_dependency_msg env sigma id err)
+ user_err "" (clear_dependency_msg env sigma id err)
let replacing_dependency_msg env sigma id = function
| Evarutil.OccurHypInSimpleClause None ->
@@ -269,7 +269,7 @@ let replacing_dependency_msg env sigma id = function
Printer.pr_existential env sigma ev ++ str"."
let error_replacing_dependency env sigma id err =
- errorlabstrm "" (replacing_dependency_msg env sigma id err)
+ user_err "" (replacing_dependency_msg env sigma id err)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him from removing variables that are
@@ -350,7 +350,7 @@ let rename_hyp repl =
let () =
try
let elt = Id.Set.choose (Id.Set.inter dst mods) in
- CErrors.errorlabstrm "" (pr_id elt ++ str " is already used")
+ CErrors.user_err "" (pr_id elt ++ str " is already used")
with Not_found -> ()
in
(** All is well *)
@@ -508,7 +508,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
if not (eq_mind sp sp') then
error "Fixpoints should be on the same mutual inductive declaration.";
if mem_named_context f (named_context_of_val sign) then
- errorlabstrm "Logic.prim_refiner"
+ user_err "Logic.prim_refiner"
(str "Name " ++ pr_id f ++ str " already used in the environment");
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
in
@@ -599,7 +599,7 @@ let pf_reduce_decl redfun where decl gl =
match decl with
| LocalAssum (id,ty) ->
if where == InHypValueOnly then
- errorlabstrm "" (pr_id id ++ str " has no value.");
+ user_err "" (pr_id id ++ str " has no value.");
LocalAssum (id,redfun' ty)
| LocalDef (id,b,ty) ->
let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -700,7 +700,7 @@ let pf_e_reduce_decl redfun where decl gl =
match decl with
| LocalAssum (id,ty) ->
if where == InHypValueOnly then
- errorlabstrm "" (pr_id id ++ str " has no value.");
+ user_err "" (pr_id id ++ str " has no value.");
let Sigma (ty', sigma, p) = redfun sigma ty in
Sigma (LocalAssum (id, ty'), sigma, p)
| LocalDef (id,b,ty) ->
@@ -740,7 +740,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
match decl with
| LocalAssum (id,ty) ->
if where == InHypValueOnly then
- errorlabstrm "" (pr_id id ++ str " has no value.");
+ user_err "" (pr_id id ++ str " has no value.");
let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
Sigma (LocalAssum (id, ty'), sigma, p)
| LocalDef (id,b,ty) ->
@@ -778,12 +778,12 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
isSort (whd_all env sigma t2)
then (mayneedglobalcheck := true; sigma)
else
- errorlabstrm "convert-check-hyp" (str "Types are incompatible.")
+ user_err "convert-check-hyp" (str "Types are incompatible.")
else sigma
end
else
if not (isSort (whd_all env sigma t1)) then
- errorlabstrm "convert-check-hyp" (str "Not a type.")
+ user_err "convert-check-hyp" (str "Not a type.")
else sigma
(* Now we introduce different instances of the previous tacticals *)
@@ -792,7 +792,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun en
let sigma = Sigma.to_evar_map sigma in
let sigma = check_types env sigma mayneedglobalcheck deep t' c in
let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
- if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
+ if not b then user_err "convert-check-hyp" (str "Not convertible.");
Sigma.Unsafe.of_pair (t', sigma)
end }
@@ -883,7 +883,7 @@ let reduce redexp cl =
let unfold_constr = function
| ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
| VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
- | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
+ | _ -> user_err "unfold_constr" (str "Cannot unfold a non-constant.")
(*******************************************)
(* Introduction tactics *)
@@ -1078,7 +1078,7 @@ let depth_of_quantified_hypothesis red h gl =
match lookup_hypothesis_as_renamed_gen red h gl with
| Some depth -> depth
| None ->
- errorlabstrm "lookup_quantified_hypothesis"
+ user_err "lookup_quantified_hypothesis"
(str "No " ++ msg_quantified_hypothesis h ++
strbrk " in current goal" ++
(if red then strbrk " even after head-reduction" else mt ()) ++
@@ -1227,7 +1227,7 @@ let cut c =
let error_uninstantiated_metas t clenv =
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
- in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
+ in user_err "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
let check_unresolved_evars_of_metas sigma clenv =
(* This checks that Metas turned into Evars by *)
@@ -1360,7 +1360,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
let indmv =
(match kind_of_term (nth_arg i elimclause.templval.rebus) with
| Meta mv -> mv
- | _ -> errorlabstrm "elimination_clause"
+ | _ -> user_err "elimination_clause"
(str "The type of elimination clause is not well-formed."))
in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
@@ -1525,7 +1525,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
try match List.remove Int.equal indmv (clenv_independent elimclause) with
| [a] -> a
| _ -> failwith ""
- with Failure _ -> errorlabstrm "elimination_clause"
+ with Failure _ -> user_err "elimination_clause"
(str "The type of elimination clause is not well-formed.") in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
let hyp = mkVar id in
@@ -1534,7 +1534,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
if Term.eq_constr hyp_typ new_hyp_typ then
- errorlabstrm "general_rewrite_in"
+ user_err "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars id id sigma elimclause''
(fun id -> Proofview.tclUNIT ())
@@ -2015,7 +2015,7 @@ let clear_body ids =
let map = function
| LocalAssum (id,t) as decl ->
let () = if List.mem_f Id.equal id ids then
- errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
+ user_err "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
in
decl
| LocalDef (id,_,t) as decl ->
@@ -2146,7 +2146,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
if Int.equal i 0 then error "The constructors are numbered starting from 1.";
begin match expctdnumopt with
| Some n when not (Int.equal n nconstr) ->
- errorlabstrm "Tactics.check_number_of_constructors"
+ user_err "Tactics.check_number_of_constructors"
(str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
| _ -> ()
end;
@@ -2725,7 +2725,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
let generalized_name c t ids cl = function
| Name id as na ->
if Id.List.mem id ids then
- errorlabstrm "" (pr_id id ++ str " is already used.");
+ user_err "" (pr_id id ++ str " is already used.");
na
| Anonymous ->
match kind_of_term c with
@@ -2886,7 +2886,7 @@ let specialize (c,lbind) ipat =
let tstack = chk tstack in
let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
if occur_meta term then
- errorlabstrm "" (str "Cannot infer an instance for " ++
+ user_err "" (str "Cannot infer an instance for " ++
pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
str ".");
@@ -2931,7 +2931,7 @@ let unfold_body x =
(** We normalize the given hypothesis immediately. *)
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
let xval = match Context.Named.lookup x hyps with
- | LocalAssum _ -> errorlabstrm "unfold_body"
+ | LocalAssum _ -> user_err "unfold_body"
(pr_id x ++ str" is not a defined hypothesis.")
| LocalDef (_,xval,_) -> xval
in
@@ -3428,7 +3428,7 @@ let make_up_names n ind_opt cname =
let error_ind_scheme s =
let s = if not (String.is_empty s) then s^" " else s in
- errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
+ user_err "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
let glob = Universes.constr_of_global
@@ -4046,7 +4046,7 @@ let recolle_clenv i params args elimclause gl =
(fun x ->
match kind_of_term x with
| Meta mv -> mv
- | _ -> errorlabstrm "elimination_clause"
+ | _ -> user_err "elimination_clause"
(str "The type of the elimination clause is not well-formed."))
arr in
let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in
@@ -4193,7 +4193,7 @@ let clear_unselected_context id inhyps cls =
let open Context.Named.Declaration in
if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
cls.concl_occs == NoOccurrences
- then errorlabstrm ""
+ then user_err ""
(str "Conclusion must be mentioned: it depends on " ++ pr_id id
++ str ".");
match cls.onhyps with
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:15:42 +0000