diff options
Diffstat (limited to 'plugins')
34 files changed, 98 insertions, 95 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 12d7f0660..b3ab29cce 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -53,9 +53,9 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> CErrors.error"Admitted isn't supported in Derive." + | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") | Proved (_,Some _,_) -> - CErrors.error"Cannot save a proof of Derive with an explicit name." + CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 322fbcea7..2c85b185c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -41,7 +41,7 @@ let toplevel_env () = | "MODULE TYPE" -> let modtype = Global.lookup_modtype (MPdot (mp, l)) in Some (l, SFBmodtype modtype) - | "INCLUDE" -> error "No extraction of toplevel Include yet." + | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.") | _ -> None end | _ -> None @@ -435,7 +435,7 @@ let mono_filename f = else try Id.of_string (Filename.basename f) with UserError _ -> - error "Extraction: provided filename is not a valid identifier" + user_err Pp.(str "Extraction: provided filename is not a valid identifier") in Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 0692c88cd..b580fb592 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -185,7 +185,7 @@ let rec pp_expr par env args = pp_boxed_tuple (pp_expr true env []) l | MLcase (_,t, pv) when is_custom_match pv -> if not (is_regular_match pv) then - error "Cannot mix yet user-given match and general patterns."; + user_err Pp.(str "Cannot mix yet user-given match and general patterns."); let mkfun (ids,_,e) = if not (List.is_empty ids) then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index d8e382155..4399fc561 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -246,7 +246,7 @@ let rec pp_expr par env args = pp_boxed_tuple (pp_expr true env []) l | MLcase (_, t, pv) when is_custom_match pv -> if not (is_regular_match pv) then - error "Cannot mix yet user-given match and general patterns."; + user_err Pp.(str "Cannot mix yet user-given match and general patterns."); let mkfun (ids,_,e) = if not (List.is_empty ids) then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 8d0cc4a0d..3c81564e3 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -96,9 +96,9 @@ let rec pp_expr env args = prlist_with_sep spc (pp_cons_args env) args') in if is_coinductive r then paren (str "delay " ++ st) else st - | MLtuple _ -> error "Cannot handle tuples in Scheme yet." + | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.") | MLcase (_,_,pv) when not (is_regular_match pv) -> - error "Cannot handle general patterns in Scheme yet." + user_err Pp.(str "Cannot handle general patterns in Scheme yet.") | MLcase (_,t,pv) when is_custom_match pv -> let mkfun (ids,_,e) = if not (List.is_empty ids) then named_lams (List.rev ids) e diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 5a1e7c26a..4c6355f61 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -161,7 +161,7 @@ let left_instance_tac (inst,id) continue seq= let evmap, _ = try Typing.type_of (pf_env gl) evmap gt with e when CErrors.noncritical e -> - error "Untypable instance, maybe higher-order non-prenex quantification" in + user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in Sigma.Unsafe.of_pair (generalize [gt], evmap) end }) else diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 2d18b6605..826afc35b 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -227,7 +227,7 @@ let extend_with_auto_hints env sigma l seq = try searchtable_map dbname with Not_found-> - error ("Firstorder: "^dbname^" : No such Hint database") in + user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in Hint_db.iter g hdb in List.iter h l; !seqref, sigma (*FIXME: forgetting about universes*) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 25d8f8c83..f397f84a8 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -513,11 +513,11 @@ let rec fourier () = with NoIneq -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.error "No inequalities"; + if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] - then CErrors.error "fourier failed" + then CErrors.user_err Pp.(str "fourier failed") (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 55d361e3d..64f7813a3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -820,10 +820,10 @@ let build_proof build_proof new_finalize {dyn_infos with info = f } g end | Fix _ | CoFix _ -> - error ( "Anonymous local (co)fixpoints are not handled yet") + user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) - | Proj _ -> error "Prod" - | Prod _ -> error "Prod" + | Proj _ -> user_err Pp.(str "Prod") + | Prod _ -> user_err Pp.(str "Prod") | LetIn _ -> let new_infos = { dyn_infos with @@ -1097,7 +1097,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Global.env ()) (Evd.empty) (EConstr.of_constr body) - | None -> error ( "Cannot define a principle over an axiom ") + | None -> user_err Pp.(str "Cannot define a principle over an axiom ") in let fbody = get_body fnames.(fun_num) in let f_ctxt,f_body = decompose_lam (project g) fbody in @@ -1199,7 +1199,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam bs.(num), List.rev_map var_of_decl princ_params)) ),num - | _ -> error "Not a mutual block" + | _ -> user_err Pp.(str "Not a mutual block") in let info = {infos with @@ -1594,7 +1594,7 @@ let prove_principle_for_gen let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with - | Undefined -> error "No tcc proof !!" + | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 529b91c4c..18d63dd94 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -75,7 +75,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let rel_as_kn = fst (match princ_type_info.indref with | Some (Globnames.IndRef ind) -> ind - | _ -> error "Not a valid predicate" + | _ -> user_err Pp.(str "Not a valid predicate") ) in let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in @@ -416,7 +416,7 @@ let get_funs_constant mp dp = in let body = EConstr.Unsafe.to_constr body in body - | None -> error ( "Cannot define a principle over an axiom ") + | None -> user_err Pp.(str ( "Cannot define a principle over an axiom ")) in let f = find_constant_body const in let l_const = get_funs_constant const f in @@ -432,7 +432,7 @@ let get_funs_constant mp dp = List.iter (fun params -> if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params) - then error "Not a mutal recursive block" + then user_err Pp.(str "Not a mutal recursive block") ) l_params in @@ -445,7 +445,7 @@ let get_funs_constant mp dp = | _ -> if is_first && Int.equal (List.length l_bodies) 1 then raise Not_Rec - else error "Not a mutal recursive block" + else user_err Pp.(str "Not a mutal recursive block") in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) @@ -454,7 +454,7 @@ let get_funs_constant mp dp = Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) - then error "Not a mutal recursive block" + then user_err Pp.(str "Not a mutal recursive block") in List.iter check l_bodies with Not_Rec -> () diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 5e6128b1b..1db8be081 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat = let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected." + | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.") ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] @@ -228,7 +228,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - CErrors.error ("Cannot generate induction principle(s)") + CErrors.user_err Pp.(str "Cannot generate induction principle(s)") | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7f2b21e79..d8614f376 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -576,8 +576,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = WARNING: We need to restart since [b] itself should be an application term *) build_entry_lc env funnames avoid (mkGApp(b,args)) - | GRec _ -> error "Not handled GRec" - | GProd _ -> error "Cannot apply a type" + | GRec _ -> user_err Pp.(str "Not handled GRec") + | GProd _ -> user_err Pp.(str "Cannot apply a type") end (* end of the application treatement *) | GLambda(n,_,t,b) -> @@ -678,7 +678,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc env funnames avoid match_expr end - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5abcb100f..0361e8cb1 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - CAst.map (function + CAst.map_with_loc (fun ?loc -> function | GRef _ as x -> x | GVar id -> let new_id = @@ -172,7 +172,7 @@ let change_vars = change_vars mapping lhs, change_vars mapping rhs ) - | GRec _ -> error "Local (co)fixes are not supported" + | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported") | GSort _ as x -> x | GHole _ as x -> x | GCast(b,c) -> @@ -352,7 +352,7 @@ let rec alpha_rt excluded rt = alpha_rt excluded lhs, alpha_rt excluded rhs ) - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ | GHole _ as rt -> rt | GCast (b,c) -> @@ -408,7 +408,7 @@ let is_free_in id = | GIf(cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | GRec _ -> raise (UserError(None,str "Not handled GRec")) + | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -695,7 +695,7 @@ let expand_as = | GIf(e,(na,po),br1,br2) -> GIf(expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) - | GRec _ -> error "Not handled GRec" + | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, Miscops.map_cast_type (expand_as map) c) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ab83cb15a..74c0eb4cc 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -186,6 +186,8 @@ let build_newrecursive l = in build_newrecursive l' +let error msg = user_err Pp.(str msg) + (* Checks whether or not the mutual bloc is recursive *) let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index ea985ddec..91dac303a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -502,13 +502,13 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match EConstr.kind sigma c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> CErrors.error "decompose_lam_n: not enough abstractions" + | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8c972cd7c..8747efc02 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -197,7 +197,7 @@ let generate_type evd g_to_f f graph i = let find_induction_principle evd f = let f_as_constant,u = match EConstr.kind !evd f with | Const c' -> c' - | _ -> error "Must be used with a function" + | _ -> user_err Pp.(str "Must be used with a function") in let infos = find_Function_infos f_as_constant in match infos.rect_lemma with @@ -701,7 +701,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) - with Not_found -> error "No graph found" + with Not_found -> user_err Pp.(str "No graph found") in if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs @@ -1006,6 +1006,7 @@ let functional_inversion kn hid fconst f_correct : tactic = | _ -> tclFAIL 1 (mt ()) g +let error msg = user_err Pp.(str msg) let invfun qhyp f = let f = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b99a05dfb..b2c8489ce 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -347,7 +347,7 @@ let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list = filter_shift_stable lnk (Array.to_list larr) - +let error msg = user_err Pp.(str msg) (** {1 Utilities for merging} *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c46309355..e206955ac 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -136,7 +136,7 @@ let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" - with Not_found -> error "module Recdef not loaded" + with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter = function () -> (constr_of_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") @@ -323,8 +323,8 @@ let check_not_nested sigma forbidden e = | Construct _ -> () | Case(_,t,e,a) -> check_not_nested t;check_not_nested e;Array.iter check_not_nested a - | Fix _ -> error "check_not_nested : Fix" - | CoFix _ -> error "check_not_nested : Fix" + | Fix _ -> user_err Pp.(str "check_not_nested : Fix") + | CoFix _ -> user_err Pp.(str "check_not_nested : Fix") in try check_not_nested e @@ -430,8 +430,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = let sigma = project g in match EConstr.kind sigma expr_info.info with - | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint" - | Proj _ -> error "Function cannot treat projections" + | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") + | Proj _ -> user_err Pp.(str "Function cannot treat projections") | LetIn(na,b,t,e) -> begin let new_continuation_tac = @@ -1304,7 +1304,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in let na = next_global_ident_away name [] in if Termops.occur_existential sigma gls_type then - CErrors.error "\"abstract\" cannot handle existentials"; + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.tag na) in diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 470a93f2b..bf84f61a5 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -56,17 +56,16 @@ let instantiate_tac n c ido = InHyp -> (match decl with | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ) - | _ -> error - "Please be more specific: in type or value?") + | _ -> user_err Pp.(str "Please be more specific: in type or value?")) | InHypTypeOnly -> evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl)) | InHypValueOnly -> (match decl with | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) - | _ -> error "Not a defined hypothesis.") in + | _ -> user_err Pp.(str "Not a defined hypothesis.")) in if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; + user_err Pp.(str "Not enough uninstantiated existential variables."); + if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in instantiate_evar evk c sigma gl end @@ -76,7 +75,7 @@ let instantiate_tac_by_name id c = let sigma = gl.sigma in let evk = try Evd.evar_key id sigma - with Not_found -> error "Unknown existential variable." in + with Not_found -> user_err Pp.(str "Unknown existential variable.") in instantiate_evar evk c sigma gl end @@ -109,8 +108,8 @@ let hget_evar n = let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; + user_err Pp.(str "Not enough uninstantiated existential variables."); + if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index a3310c2d8..fdb8d3461 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -90,7 +90,7 @@ let occurrences_of = function | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) | nl -> if List.exists (fun n -> n < 0) nl then - CErrors.error "Illegal negative occurrence number."; + CErrors.user_err Pp.(str "Illegal negative occurrence number."); OnlyOccurrences nl let coerce_to_int v = match Value.to_int v with diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index cbd8a7f0f..ed80dd7ae 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1084,7 +1084,7 @@ let decompose l c = let sigma = Tacmach.New.project gl in let to_ind c = if isInd sigma c then fst (destInd sigma c) - else error "not an inductive type" + else user_err Pp.(str "not an inductive type") in let l = List.map to_ind l in Elim.h_decompose l c diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 257100b01..1404b1c1f 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -117,8 +117,8 @@ let mk_fix_tac (loc,id,bl,ann,ty) = | _, Some x -> let ids = List.map snd (List.flatten (List.map pi1 bl)) in (try List.index Names.Name.equal (snd x) ids - with Not_found -> error "No such fix variable.") - | _ -> error "Cannot guess decreasing argument of fix." in + with Not_found -> user_err Pp.(str "No such fix variable.")) + | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = @@ -152,7 +152,7 @@ let mkTacCase with_evar = function | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then - error "Use of numbers as direct arguments of 'case' is not supported."; + user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported."); TacInductionDestruct (false,with_evar,ic) let rec mkCLambdaN_simple_loc ?loc bll c = diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 75ab1c5ee..a001c6a2b 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -348,7 +348,7 @@ type 'a extra_genarg_printer = let bll = List.map (fun (x, _, y) -> x, y) bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a - | _ -> error "Cannot translate fix tactic: not enough products" in + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_ltac_or_var pr = function @@ -1089,7 +1089,7 @@ type 'a extra_genarg_printer = match ty.CAst.v with Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let raw_printers = @@ -1160,7 +1160,7 @@ type 'a extra_genarg_printer = match Term.kind_of_term ty with Term.Prod(na,a,b) -> strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_atomic_tactic_level env sigma n t = @@ -1210,7 +1210,7 @@ let declare_extra_genarg_pprule wit (h : 'c extra_genarg_printer) = begin match wit with | ExtraArg s -> () - | _ -> error "Can declare a pretty-printing rule only for extra argument types." + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in let g x = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e8c9f4eba..51729f4c6 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -241,7 +241,7 @@ end) = struct let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs - else error "build_signature: no constraint can apply on a dependent argument" + else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") | _, [] -> (match finalcstr with @@ -478,7 +478,7 @@ type hypinfo = { let get_symmetric_proof b = if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof -let error_no_relation () = error "Cannot find a relation to rewrite." +let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.") let rec decompose_app_rel env evd t = (** Head normalize for compatibility with the old meta mechanism *) @@ -531,7 +531,7 @@ let decompose_applied_relation env sigma (c,l) = let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c - | None -> error "Cannot find an homogeneous relation to rewrite." + | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.") let rewrite_db = "rewrite" @@ -837,7 +837,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then - error "Cannot rewrite inside dependent arguments of a function"; + user_err Pp.(str "Cannot rewrite inside dependent arguments of a function"); x :: acc, x :: subst, evars, sigargs, x :: typeargs') ([], [], evars, sigargs, []) args args' in @@ -1425,7 +1425,7 @@ module Strategies = let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> - error "fold: the term is not unfoldable !" + user_err Pp.(str "fold: the term is not unfoldable !") in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in @@ -2204,7 +2204,7 @@ let setoid_symmetry_in id = let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "Cannot find an equivalence relation to rewrite." + | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.") in let others,(c1,c2) = split_last_two args in let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4d7b0f929..75f89a81e 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -60,7 +60,7 @@ let get_tacentry n m = else EntryName (rawwit Tacarg.wit_tactic, atactic n) let get_separator = function -| None -> error "Missing separator." +| None -> user_err Pp.(str "Missing separator.") | Some sep -> sep let rec parse_user_entry s sep = @@ -110,7 +110,7 @@ let get_tactic_entry n = else if 1<=n && n<5 then Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) else - error ("Invalid Tactic Notation level: "^(string_of_int n)^".") + user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) (**********************************************************************) (** State of the grammar extensions *) @@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state = in let () = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then - error "Notation for simple tactic must start with an identifier." + user_err Pp.(str "Notation for simple tactic must start with an identifier.") in let map = function | TacTerm s -> GramTerminal s @@ -208,7 +208,7 @@ let interp_prod_item = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names else begin match ArgT.name s with - | None -> error ("Unknown entry "^s^".") + | None -> user_err Pp.(str ("Unknown entry "^s^".")) | Some arg -> arg end | Some n -> @@ -253,8 +253,8 @@ let pprule pa = { let check_key key = if Tacenv.check_alias key then - error "Conflicting tactic notations keys. This can happen when including \ - twice the same module." + user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \ + twice the same module.") let cache_tactic_notation (_, tobj) = let key = tobj.tacobj_key in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 6c7eb8c89..e431a13bc 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -252,7 +252,7 @@ and intern_or_and_intro_pattern lf ist = function let intern_or_and_intro_pattern_loc lf ist = function | ArgVar (_,id) as x -> if find_var id ist then x - else error "Disjunctive/conjunctive introduction pattern expected." + else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) let intern_intro_pattern_naming_loc lf ist (loc,pat) = diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 632b9dac1..af8107025 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -462,7 +462,7 @@ let theoremedeszeros_termes lp = lexico:=true; |7 -> sinfo "ordre lexico computation with sugar, division by pairs"; lexico:=true; - | _ -> error "nsatz: bad parameter" + | _ -> user_err Pp.(str "nsatz: bad parameter") ); let lvar = List.init nvars (fun i -> Printf.sprintf "x%i" (i + 1)) in let lvar = ["a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z"] @ lvar in @@ -549,5 +549,5 @@ let nsatz_compute t = let lpol = try nsatz t with Ideal.NotInIdeal -> - error "nsatz cannot solve this problem" in + user_err Pp.(str "nsatz cannot solve this problem") in return_term lpol diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 334baec8d..d3ca874bd 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -456,7 +456,7 @@ let destructurate_prop sigma t = Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) - | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" + | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") | _ -> Kufo let destructurate_type sigma t = @@ -891,7 +891,7 @@ let rec scalar p n = function (Lazy.force coq_fast_Zmult_assoc_reverse); focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (n*x)) - | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") | (Oatom _ as t) -> [], Otimes(t,Oz n) | Oz i -> [focused_simpl p],Oz(n*i) | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |])) @@ -943,7 +943,7 @@ let rec negate p = function [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] (Lazy.force coq_fast_Zopp_mult_distr_r); focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x)) - | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products" + | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products") | (Oatom _ as t) -> let r = Otimes(t,Oz(negone)) in [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r @@ -1026,7 +1026,7 @@ let shrink_pair p f1 f2 = | t1,t2 -> begin oprint t1; print_newline (); oprint t2; print_newline (); - flush Pervasives.stdout; error "shrink.1" + flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1") end let reduce_factor p = function @@ -1038,10 +1038,10 @@ let reduce_factor p = function let rec compute = function | Oz n -> n | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2) - | _ -> error "condense.1" + | _ -> CErrors.user_err Pp.(str "condense.1") in [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) - | t -> oprint t; error "reduce_factor.1" + | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1") let rec condense p = function | Oplus(f1,(Oplus(f2,r) as t)) -> diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 6b711a176..ce7ffb1e7 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -35,7 +35,7 @@ let omega_tactic l = | "positive" -> eval_tactic "zify_positive" | "N" -> eval_tactic "zify_N" | "Z" -> eval_tactic "zify_op" - | s -> CErrors.error ("No Omega knowledge base for type "^s)) + | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index c649cfb2c..db69f1b40 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -183,7 +183,7 @@ type inversion_scheme = { goal [gl]. This function uses the auxiliary functions [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) -let i_can't_do_that () = error "Quote: not a simple fixpoint" +let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint") let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c) diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index c2d7d5050..6479c683b 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -28,7 +28,7 @@ let romega_tactic unsafe l = | "positive" -> eval_tactic "zify_positive" | "N" -> eval_tactic "zify_N" | "Z" -> eval_tactic "zify_op" - | s -> CErrors.error ("No ROmega knowledge base for type "^s)) + | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e56605076..fdcd62299 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1042,5 +1042,5 @@ let total_reflexive_omega_tactic unsafe = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution unsafe env reified_goal systems_list - with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" + with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") end } diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e20e78b1a..0e1225ada 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -8,7 +8,6 @@ open Ltac_plugin open Pp -open CErrors open Util open Names open Term @@ -32,6 +31,8 @@ open Misctypes open Newring_ast open Proofview.Notations +let error msg = CErrors.user_err Pp.(str msg) + (****************************************************************************) (* controlled reduction *) @@ -46,7 +47,7 @@ let tag_arg tag_rec map subs i c = let global_head_of_constr sigma c = let f, args = decompose_app sigma c in try fst (Termops.global_of_constr sigma f) - with Not_found -> anomaly (str "global_head_of_constr") + with Not_found -> CErrors.anomaly (str "global_head_of_constr") let global_of_constr_nofail c = try global_of_constr c @@ -82,7 +83,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") + CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in @@ -359,13 +360,13 @@ let find_ring_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err ~hdr:"ring" + CErrors.user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - user_err ~hdr:"ring" + CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false @@ -852,13 +853,13 @@ let find_field_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err ~hdr:"field" + CErrors.user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - user_err ~hdr:"field" + CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 862e44cca..6b752fb4b 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -468,7 +468,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = | Evar (k, _) -> if Evd.mem sigma0 k then KpatEvar k, f, a else if a <> [] then KpatFlex, f, a else - (match p_origin with None -> CErrors.error "indeterminate pattern" + (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern") | Some (dir, rule) -> errorstrm (str "indeterminate " ++ pr_dir_side dir ++ str " in " ++ pr_constr_pat rule)) @@ -1320,7 +1320,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let fill_occ_term env cl occ sigma0 (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in - if sigma' != sigma0 then CErrors.error "matching impacts evars" + if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars") else cl, (Evd.merge_universe_context sigma' uc, t') with NoMatch -> try let sigma', uc, t' = |