diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 2c97cf442..4391a96b1 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 |