diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
| commit | 4c1260299b707bd27765b0ab365092046b134a69 (patch) | |
| tree | 22331e8562bee137a5d2eea79c0d8e3d43cb94c1 | |
| parent | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (diff) | |
| parent | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (diff) | |
Merge PR#512: [cleanup] Unify all calls to the error function.
116 files changed, 437 insertions, 421 deletions
diff --git a/checker/check.ml b/checker/check.ml index 11678fa6b..6d93c11ea 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -72,7 +72,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (DirPath.to_string dir)) + user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir))) let library_full_filename dir = (find_library dir).library_filename diff --git a/checker/checker.ml b/checker/checker.ml index 5cadfe7b9..e00f47a54 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -335,7 +335,7 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); print_endline (Envars.coqlib ()); exit 0 @@ -373,7 +373,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); if_verbose print_header (); init_load_path (); engage (); diff --git a/checker/environ.ml b/checker/environ.ml index 7b59c6b98..bce40861c 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -45,7 +45,7 @@ let set_engagement (impr_set as c) env = env.env_stratification.env_engagement in begin match impr_set,expected_impr_set with - | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement" + | PredicativeSet, ImpredicativeSet -> user_err Pp.(str "Incompatible engagement") | _ -> () end; { env with env_stratification = diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 27f79e796..0482912b0 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -535,13 +535,13 @@ let check_inductive env kn mib = (* check mind_finite : always OK *) (* check mind_ntypes *) if Array.length mib.mind_packets <> mib.mind_ntypes then - error "not the right number of packets"; + user_err Pp.(str "not the right number of packets"); (* check mind_params_ctxt *) let params = mib.mind_params_ctxt in let _ = check_ctxt env params in (* check mind_nparams *) if rel_context_nhyps params <> mib.mind_nparams then - error "number the right number of parameters"; + user_err Pp.(str "number the right number of parameters"); (* mind_packets *) (* - check arities *) let env_ar = typecheck_arity env params mib.mind_packets in diff --git a/checker/inductive.ml b/checker/inductive.ml index 8f23a38af..9e417a8eb 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -27,7 +27,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body let lookup_mind_specif env (kn,tyi) = let mib = lookup_mind kn env in if tyi >= Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = @@ -232,7 +232,7 @@ let type_of_constructor_subst cstr u (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = diff --git a/checker/modops.ml b/checker/modops.ml index 07dda8a06..bed31143b 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -16,21 +16,21 @@ open Declarations (*i*) let error_not_a_constant l = - error ("\""^(Label.to_string l)^"\" is not a constant") + user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant")) -let error_not_a_functor () = error "Application of not a functor" +let error_not_a_functor () = user_err Pp.(str "Application of not a functor") -let error_incompatible_modtypes _ _ = error "Incompatible module types" +let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types") let error_not_match l _ = - error ("Signature components for label "^Label.to_string l^" do not match") + user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match")) -let error_no_such_label l = error ("No such label "^Label.to_string l) +let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l)) let error_no_such_label_sub l l1 = let l1 = ModPath.to_string l1 in - error ("The field "^ - Label.to_string l^" is missing in "^l1^".") + user_err Pp.(str ("The field "^ + Label.to_string l^" is missing in "^l1^".")) let error_not_a_module_loc ?loc s = user_err ?loc (str ("\""^Label.to_string s^"\" is not a module")) @@ -38,7 +38,7 @@ let error_not_a_module_loc ?loc s = let error_not_a_module s = error_not_a_module_loc s let error_with_module () = - error "Unsupported 'with' constraint in module implementation" + user_err Pp.(str "Unsupported 'with' constraint in module implementation") let is_functor = function | MoreFunctor _ -> true diff --git a/checker/reduction.ml b/checker/reduction.ml index 28c0126b4..82f09cf4b 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -536,5 +536,5 @@ let dest_arity env c = let l, c = dest_prod_assum env c in match c with | Sort s -> l,s - | _ -> error "not an arity" + | _ -> user_err Pp.(str "not an arity") diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 53d80c6d5..c70cd5c8c 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end; () @@ -61,7 +61,7 @@ let check_imports f caller env needed = let actual_stamp = lookup_digest env dp in if stamp <> actual_stamp then report_clash f caller dp with Not_found -> - error ("Reference to unknown module " ^ (DirPath.to_string dp)) + user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp))) in Array.iter check needed diff --git a/checker/subtyping.ml b/checker/subtyping.ml index a290b240d..2d04b77e4 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -302,22 +302,22 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "name.")); + "name."))); if constant_has_body cb2 then error () ; let u = inductive_instance mind1 in let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "name.")); + "name."))); if constant_has_body cb2 then error () ; let u1 = inductive_instance mind1 in let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in diff --git a/checker/term.ml b/checker/term.ml index 24e6008d3..8cac78375 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -273,14 +273,14 @@ let decompose_lam = abstractions *) let decompose_lam_n_assum n = if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match c with | Lambda (x,t,c) -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec empty_rel_context n @@ -306,14 +306,14 @@ let decompose_prod_assum = let decompose_prod_n_assum n = if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else match c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions") in prodec_rec empty_rel_context n diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index bb6c2f660..7fad65bf0 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -175,7 +175,7 @@ uses type classes and rejects terms with unresolved holes. functions that used to carry a suffix `_loc`, such suffix has been dropped. -- `errorlabstrm` has been removed in favor of `user_err`. +- `errorlabstrm` and `error` has been removed in favor of `user_err`. - The header parameter to `user_err` has been made optional. diff --git a/engine/eConstr.ml b/engine/eConstr.ml index e5ac3792d..c0485e4e7 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -295,7 +295,7 @@ let decompose_lam_assum sigma c = let decompose_lam_n_assum sigma n c = let open Rel.Declaration in if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -303,14 +303,14 @@ let decompose_lam_n_assum sigma n c = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n c let decompose_lam_n_decls sigma n = let open Rel.Declaration in if n < 0 then - error "decompose_lam_n_decls: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_decls: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -318,7 +318,7 @@ let decompose_lam_n_decls sigma n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_decls: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n @@ -363,7 +363,7 @@ let decompose_prod_assum sigma c = let decompose_prod_n_assum sigma n c = let open Rel.Declaration in if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else @@ -371,7 +371,7 @@ let decompose_prod_n_assum sigma n c = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n c diff --git a/engine/evd.ml b/engine/evd.ml index 8ade6cb99..b677705bc 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -952,7 +952,7 @@ let declare_principal_goal evk evd = | None -> { evd with future_goals = evk::evd.future_goals; principal_future_goal=Some evk; } - | Some _ -> CErrors.error "Only one main subgoal per instantiation." + | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") let future_goals evd = evd.future_goals diff --git a/engine/proofview.ml b/engine/proofview.ml index 7f80d40d6..ddfc0e39d 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -289,7 +289,7 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success." + | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") | _ -> raise CErrors.Unhandled end diff --git a/engine/uState.ml b/engine/uState.ml index dc6822057..acef90143 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -188,7 +188,7 @@ let process_universe_constraints ctx cstrs = | _ -> local else begin match Univ.Universe.level r with - | None -> error ("Algebraic universe on the right") + | None -> user_err Pp.(str "Algebraic universe on the right") | Some r' -> if Univ.Level.is_small r' then let levels = Univ.Universe.levels l in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c7078cf2a..4dcf287ef 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -579,7 +579,7 @@ let rec subordinate_letins letins = function let terms_of_binders bl = let rec term_of_pat pt = CAst.map_with_loc (fun ?loc -> function | PatVar (Name id) -> CRef (Ident (loc,id), None) - | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term." + | PatVar (Anonymous) -> user_err Pp.(str "Cannot turn \"_\" into a term.") | PatCstr (c,l,_) -> let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in @@ -589,7 +589,7 @@ let terms_of_binders bl = | {loc; v = GLocalAssum (Name id,_,_)}::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l | {loc; v = GLocalDef (Name id,_,_,_)}::l -> extract_variables l | {loc; v = GLocalDef (Anonymous,_,_,_)}::l - | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> error "Cannot turn \"_\" into a term." + | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> user_err Pp.(str "Cannot turn \"_\" into a term.") | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l | [] -> [] in extract_variables bl @@ -1862,7 +1862,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let eargs, rargs = extract_explicit_arg l args in if !parsing_explicit then if Id.Map.is_empty eargs then intern_args env subscopes rargs - else error "Arguments given by name or position not supported in explicit mode." + else user_err Pp.(str "Arguments given by name or position not supported in explicit mode.") else let rec aux n impl subscopes eargs rargs = let (enva,subscopes') = apply_scope_env env subscopes in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 74644b206..6f9100911 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -42,7 +42,7 @@ let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ | _,(GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> error "Unsupported construction in recursive notations." + -> user_err Pp.(str "Unsupported construction in recursive notations.") | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ | GHole _ | GSort _ | GLetIn _), _ -> false @@ -112,7 +112,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with (* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function - | Anonymous -> CErrors.error "This expression should be a simple identifier." + | Anonymous -> CErrors.user_err Pp.(str "This expression should be a simple identifier.") | Name id -> id let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na @@ -377,7 +377,7 @@ let notation_constr_and_vars_of_glob_constr a = Array.iter (add_id found) idl; let dll = Array.map (List.map (fun (na,bk,oc,b) -> if bk != Explicit then - error "Binders marked as implicit not allowed in notations."; + user_err Pp.(str "Binders marked as implicit not allowed in notations."); add_name found na; (na,Option.map aux oc,aux b))) dll in NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k) @@ -387,7 +387,7 @@ let notation_constr_and_vars_of_glob_constr a = NHole (w, naming, arg) | GRef (r,_) -> NRef r | GEvar _ | GPatVar _ -> - error "Existential variables not allowed in notations." + user_err Pp.(str "Existential variables not allowed in notations.") ) x in let t = aux a in @@ -415,9 +415,9 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = Id.List.mem_assoc_sym x foundrec || Id.List.mem_assoc_sym x foundrecbinding then - error + user_err Pp.(str (Id.to_string x ^ - " should not be bound in a recursive pattern of the right-hand side.") + " should not be bound in a recursive pattern of the right-hand side.")) else injective := false in let check_pair s x y where = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1fe63c19c..a79f10df6 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -163,7 +163,7 @@ let split_at_annot bl na = match na with | None -> begin match names with - | [] -> error "A fixpoint needs at least one parameter." + | [] -> user_err (Pp.str "A fixpoint needs at least one parameter.") | _ -> ([], bl) end | Some (loc, id) -> diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 3f1cf9248..453316980 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = | _ -> Cpred.add c oracle.cst_trstate in { oracle with cst_opacity; cst_trstate; } - | RelKey _ -> CErrors.error "set_strategy: RelKey" + | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey") let fold_strategy f { var_opacity; cst_opacity; } accu = let fvar id lvl accu = f (VarKey id) lvl accu in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d8d365c34..4f4b641b4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -25,7 +25,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body let lookup_mind_specif env (kn,tyi) = let mib = Environ.lookup_mind kn env in if tyi >= Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = @@ -247,7 +247,7 @@ let type_of_constructor (cstr, u) (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = diff --git a/kernel/names.ml b/kernel/names.ml index f5b3f4e00..afdbe0c0d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -35,7 +35,7 @@ struct let hash = String.hash let check_valid ?(strict=true) x = - let iter (fatal, x) = if fatal || strict then CErrors.error x in + let iter (fatal, x) = if fatal || strict then CErrors.user_err Pp.(str x) in Option.iter iter (Unicode.ident_refutation x) let is_valid s = match Unicode.ident_refutation s with diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 6bd82170e..26d061768 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -125,7 +125,7 @@ let call_linker ?(fatal=true) prefix f upds = if not (Sys.file_exists f) then begin let msg = "Cannot find native compiler file " ^ f in - if fatal then CErrors.error msg + if fatal then CErrors.user_err Pp.(str msg) else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index d0593c0e0..502a10113 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -36,12 +36,11 @@ let empty_opaquetab = { (* hooks *) let default_get_opaque dp _ = - CErrors.error - ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) + CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp]) let default_get_univ dp _ = - CErrors.error - ("Cannot access universe constraints of opaque proofs in library " ^ - DirPath.to_string dp) + CErrors.user_err (Pp.pr_sequence Pp.str [ + "Cannot access universe constraints of opaque proofs in library "; + DirPath.to_string dp]) let get_opaque = ref default_get_opaque let get_univ = ref default_get_univ diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index caaaff1b8..f5e8e8653 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -192,7 +192,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end @@ -346,10 +346,10 @@ let check_required current_libs needed = try let actual = DPMap.find id current_libs in if not(digest_match ~actual ~required) then - CErrors.error - ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str + ["Inconsistent assumptions over module"; DirPath.to_string id; "."]) with Not_found -> - CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str ["Reference to unknown module"; DirPath.to_string id; "."]) in Array.iter check needed @@ -367,7 +367,7 @@ let safe_push_named d env = let _ = try let _ = Environ.lookup_named id env in - CErrors.error ("Identifier "^Id.to_string id^" already defined.") + CErrors.user_err Pp.(pr_sequence str ["Identifier"; Id.to_string id; "already defined."]) with Not_found -> () in Environ.push_named d env @@ -908,7 +908,7 @@ let register_inline kn senv = let open Environ in let open Pre_env in if not (evaluable_constant kn senv.env) then - CErrors.error "Register inline: an evaluable constant is expected"; + CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = pre_env senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d0fdf9fda..f779f68be 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -110,8 +110,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let u = if poly then - CErrors.error ("Checking of subtyping of polymorphic" ^ - " inductive types not implemented") + CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented") else Instance.empty in let mib2 = Declareops.subst_mind_body subst2 mib2 in @@ -347,7 +346,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Mod_subst.force_constr lc2 in check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -364,7 +363,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 03562d9f3..a4296a530 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -526,26 +526,26 @@ let decompose_lam = (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_prod_n n = - if n < 0 then error "decompose_prod_n: integer parameter must be positive"; + if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | _ -> error "decompose_prod_n: not enough products" + | _ -> user_err (str "decompose_prod_n: not enough products") in prodec_rec [] n (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_lam_n n = - if n < 0 then error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then user_err (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 kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> error "decompose_lam_n: not enough abstractions" + | _ -> user_err (str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n @@ -581,7 +581,7 @@ let decompose_lam_assum = ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *) let decompose_prod_n_assum n = if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err (str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else @@ -590,7 +590,7 @@ let decompose_prod_n_assum n = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err (str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n @@ -602,7 +602,7 @@ let decompose_prod_n_assum n = but n is the actual number of destructurated lambdas. *) let decompose_lam_n_assum n = if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err (str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -611,14 +611,14 @@ let decompose_lam_n_assum n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err (str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n (* Same, counting let-in *) let decompose_lam_n_decls n = if n < 0 then - error "decompose_lam_n_decls: integer parameter must be positive"; + user_err (str "decompose_lam_n_decls: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -627,7 +627,7 @@ let decompose_lam_n_decls n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_decls: not enough abstractions" + | c -> user_err (str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b55fd80c6..b0e77a4c9 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -38,7 +38,6 @@ exception UserError of string option * std_ppcmds (* User errors *) let todo s = prerr_string ("TODO: "^s^"\n") let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) -let error string = user_err (str string) let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) @@ -138,3 +137,8 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false + +(* Deprecated functions *) +let error string = user_err (str string) +let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg +let errorlabstrm hdr msg = user_err ~hdr msg diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 0665a8ce7..ca0838575 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -41,9 +41,6 @@ val user_err : ?loc:Loc.t -> ?hdr:string -> std_ppcmds -> 'a (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an error [pp] with optional header and location [hdr] [loc] *) -val error : string -> 'a -(** [error s] just calls [user_error "_" (str s)] *) - exception AlreadyDeclared of std_ppcmds val alreadydeclared : std_ppcmds -> 'a @@ -98,3 +95,14 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool + +(** Deprecated functions *) +val error : string -> 'a + [@@ocaml.deprecated "use [user_err] instead"] + +val errorlabstrm : string -> std_ppcmds -> 'a + [@@ocaml.deprecated "use [user_err ~hdr] instead"] + +val user_err_loc : Loc.t * string * std_ppcmds -> 'a + [@@ocaml.deprecated "use [user_err ~loc] instead"] + diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 2755946ab..d004fd671 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -86,7 +86,7 @@ let parse_flag s = | '+' -> (AsError, String.sub s 1 (String.length s - 1)) | '-' -> (Disabled, String.sub s 1 (String.length s - 1)) | _ -> (Enabled, s) - else CErrors.error "Invalid warnings flag" + else CErrors.user_err Pp.(str "Invalid warnings flag") let string_of_flag (status,name) = match status with diff --git a/library/declaremods.ml b/library/declaremods.ml index 3a263b1e1..08c33b5c1 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -345,7 +345,7 @@ let get_applications mexpr = let rec get params = function | MEident mp -> mp, params | MEapply (fexpr, mp) -> get (mp::params) fexpr - | MEwith _ -> error "Non-atomic functor application." + | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") in get [] mexpr (** Create the substitution corresponding to some functor applications *) @@ -353,7 +353,7 @@ let get_applications mexpr = let rec compute_subst env mbids sign mp_l inl = match mbids,mp_l with | _,[] -> mbids,empty_subst - | [],r -> error "Application of a functor with too few arguments." + | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") | mbid::mbids,mp::mp_l -> let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mb = Environ.lookup_module mp env in @@ -777,7 +777,7 @@ let rec decompose_functor mpl typ = match mpl, typ with | [], _ -> typ | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str - | _ -> error "Application of a functor with too much arguments." + | _ -> user_err Pp.(str "Application of a functor with too much arguments.") exception NoIncludeSelf diff --git a/library/goptions.ml b/library/goptions.ml index 9b4fc9985..a803771cb 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -71,7 +71,7 @@ module MakeTable = let _ = if String.List.mem_assoc nick !A.table then - error "Sorry, this table name is already used." + user_err Pp.(str "Sorry, this table name is already used.") module MySet = Set.Make (struct type t = A.t let compare = A.compare end) @@ -214,11 +214,11 @@ let get_option key = OptionMap.find key !value_tab let check_key key = try let _ = get_option key in - error "Sorry, this option name is already used." + user_err Pp.(str "Sorry, this option name is already used.") with Not_found -> if String.List.mem_assoc (nickname key) !string_table || String.List.mem_assoc (nickname key) !ref_table - then error "Sorry, this option name is already used." + then user_err Pp.(str "Sorry, this option name is already used.") open Libobject @@ -307,7 +307,7 @@ let set_option_value locality check_and_cast key v = | Some (name, depr, (read,write,append)) -> write (get_locality locality) (check_and_cast v (read ())) -let bad_type_error () = error "Bad type of value for this option." +let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") let check_int_value v = function | IntValue _ -> IntValue v diff --git a/library/impargs.ml b/library/impargs.ml index a63264b66..885185da1 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -364,7 +364,7 @@ let set_manual_implicits env flags enriching autoimps l = with Not_found -> l, None in if not (List.distinct l) then - error ("Some parameters are referred more than once."); + user_err Pp.(str "Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) let rec merge k l = function | (Name id,imp)::imps -> @@ -658,7 +658,7 @@ let check_inclusion l = let rec aux = function | n1::(n2::_ as nl) -> if n1 <= n2 then - error "Sequences of implicit arguments must be of different lengths."; + user_err Pp.(str "Sequences of implicit arguments must be of different lengths."); aux nl | _ -> () in aux (List.map (fun (imps,_) -> List.length imps) l) diff --git a/library/lib.ml b/library/lib.ml index ddd2ed6af..4ad4e261d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -76,7 +76,7 @@ let classify_segment seg = (* LEM; TODO: Understand what this does and see if what I do is the correct thing for ClosedMod(ule|type) *) | (_,ClosedModule _) :: stk -> clean acc stk - | (_,OpenedSection _) :: _ -> error "there are still opened sections" + | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" (str "there are still opened " ++ str (module_kind ty) ++ str "s") @@ -184,7 +184,7 @@ let split_lib_gen test = | [] -> None in match findeq [] !lib_state.lib_stk with - | None -> error "no such entry" + | None -> user_err Pp.(str "no such entry") | Some r -> r let eq_object_name (fp1, kn1) (fp2, kn2) = @@ -222,7 +222,7 @@ let add_anonymous_entry node = let add_leaf id obj = if Names.ModPath.equal (current_mp ()) Names.initial_path then - error ("No session module started (use -top dir)"); + user_err Pp.(str "No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); add_entry oname (Leaf obj); @@ -272,8 +272,8 @@ let current_mod_id () = try match find_entry_p is_opening_node_or_lib with | oname,OpenedModule (_,_,_,fs) -> basename (fst oname) | oname,CompilingLibrary _ -> basename (fst oname) - | _ -> error "you are not in a module" - with Not_found -> error "no opened modules" + | _ -> user_err Pp.(str "you are not in a module") + with Not_found -> user_err Pp.(str "no opened modules") let start_mod is_type export id mp fs = @@ -305,7 +305,7 @@ let end_mod is_type = else error_still_opened (module_kind ty) oname | oname,OpenedSection _ -> error_still_opened "section" oname | _ -> assert false - with Not_found -> error "No opened modules." + with Not_found -> user_err (Pp.str "No opened modules.") in let (after,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; @@ -326,9 +326,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after (* TODO: use check_for_module ? *) let start_compilation s mp = if !lib_state.comp_name != None then - error "compilation unit is already started"; + user_err Pp.(str "compilation unit is already started"); if not (Names.DirPath.is_empty (current_sections ())) then - error "some sections are already opened"; + user_err Pp.(str "some sections are already opened"); let prefix = s, (mp, Names.DirPath.empty) in let () = add_anonymous_entry (CompilingLibrary prefix) in lib_state := { !lib_state with comp_name = Some s; @@ -337,7 +337,7 @@ let start_compilation s mp = let end_compilation_checks dir = let _ = try match snd (find_entry_p is_opening_node) with - | OpenedSection _ -> error "There are some open sections." + | OpenedSection _ -> user_err Pp.(str "There are some open sections.") | OpenedModule (ty,_,_,_) -> user_err ~hdr:"Lib.end_compilation_checks" (str "There are some open " ++ str (module_kind ty) ++ str "s.") @@ -394,7 +394,7 @@ let find_opening_node id = user_err ~hdr:"Lib.find_opening_node" (str "Last block to end has name " ++ pr_id id' ++ str "."); entry - with Not_found -> error "There is nothing to end." + with Not_found -> user_err Pp.(str "There is nothing to end.") (* Discharge tables *) @@ -428,7 +428,7 @@ let add_section () = let check_same_poly p vars = let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in if List.exists pred vars then - error "Cannot mix universe polymorphic and monomorphic declarations in sections." + user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") let add_section_variable id impl poly ctx = match !sectab with @@ -555,7 +555,7 @@ let close_section () = | oname,OpenedSection (_,fs) -> oname,fs | _ -> assert false with Not_found -> - error "No opened section." + user_err Pp.(str "No opened section.") in let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; diff --git a/library/libnames.ml b/library/libnames.ml index dd74e192f..50f28b020 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -58,14 +58,14 @@ let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p) let parse_dir s = let len = String.length s in let rec decoupe_dirs dirs n = - if Int.equal n len && n > 0 then error (s ^ " is an invalid path."); + if Int.equal n len && n > 0 then user_err Pp.(str @@ s ^ " is an invalid path."); if n >= len then dirs else let pos = try String.index_from s n '.' with Not_found -> len in - if Int.equal pos n then error (s ^ " is an invalid path."); + if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path."); let dir = String.sub s n (pos-n) in decoupe_dirs ((Id.of_string dir)::dirs) (pos+1) in diff --git a/library/library.ml b/library/library.ml index 2b3381fa7..5a5f99cc5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -764,7 +764,7 @@ let save_library_to ?todo dir f otab = if !Flags.native_compiler then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then - error "Could not compile the library to native code." + user_err Pp.(str "Could not compile the library to native code.") with reraise -> let reraise = CErrors.push reraise in let () = Feedback.msg_warning (str "Removed file " ++ str f') in diff --git a/library/nametab.ml b/library/nametab.ml index 1027e291c..2e4e98013 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -143,8 +143,8 @@ struct (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) (* But ours is also absolute! This is an error! *) - error ("Cannot mask the absolute name \"" - ^ U.to_string uname' ^ "\"!") + user_err Pp.(str @@ "Cannot mask the absolute name \"" + ^ U.to_string uname' ^ "\"!") | Nothing | Relative _ -> mktree (Absolute (uname,o)) tree.map diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b5d0780bd..893605499 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -660,7 +660,7 @@ GEXTEND Gram if Option.is_empty !slash_position then (slash_position := Some i; parse_args i args) else - error "The \"/\" modifier can occur only once" + user_err Pp.(str "The \"/\" modifier can occur only once") in let args = parse_args 0 (List.flatten args) in let more_implicits = Option.default [] more_implicits in @@ -734,7 +734,7 @@ GEXTEND Gram | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x - | Some _, Some _ -> error "scope declared twice" in + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; @@ -742,7 +742,7 @@ GEXTEND Gram | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x - | Some _, Some _ -> error "scope declared twice" in + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; @@ -750,7 +750,7 @@ GEXTEND Gram | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x - | Some _, Some _ -> error "scope declared twice" in + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; @@ -939,7 +939,7 @@ GEXTEND Gram PrintGrammar ent | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir | IDENT "Modules" -> - error "Print Modules is obsolete; use Print Libraries instead" + user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") | IDENT "Libraries" -> PrintModules | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath 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 5cac3cbaf..a6290cb00 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -514,11 +514,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 f8c7f98f6..434fb14a6 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 (Universes.constr_of_global @@ 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 fa246ade8..68e097fe9 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 90a082d1e..2476478ab 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -510,13 +510,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 8eaa9b0f5..d68bdc215 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 00020609e..2f9f70876 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -138,7 +138,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") @@ -325,8 +325,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 @@ -432,8 +432,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 = @@ -1306,7 +1306,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 5273eb3b5..d68139a4b 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1085,7 +1085,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 b0db2839b..966b11d0e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -235,7 +235,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 @@ -472,7 +472,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 *) @@ -525,7 +525,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" @@ -831,7 +831,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 @@ -1419,7 +1419,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 @@ -2198,7 +2198,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 3a0d1dcbc..6ba4c0f93 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -464,7 +464,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 @@ -551,5 +551,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 27ce0103a..ee748567b 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 def9ff3a7..7412de1e8 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -184,7 +184,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 0cb72cc3a..38f05978d 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' = diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index edcfa99c8..2cb837ba0 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -220,9 +220,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PSoApp (n,args),m -> let fold (ans, seen) = function | PRel n -> - let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in + let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in (n :: ans, Int.Set.add n seen) - | _ -> error "Only bound indices allowed in second order pattern matching." + | _ -> user_err (str "Only bound indices allowed in second order pattern matching.") in let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in let frels = free_rels sigma cT in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index af84b70a3..bf62cea6b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1076,7 +1076,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> - error "Cannot force abstraction on identity instance." + user_err Pp.(str "Cannot force abstraction on identity instance.") | None -> make_subst (ctxt',l,occsl) end @@ -1095,7 +1095,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let set_var k = match occs with | Some Locus.AllOccurrences -> mkVar id - | Some _ -> error "Selection of specific occurrences not supported" + | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in @@ -1133,10 +1133,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* This is an arbitrary choice *) let evd = Evd.define evk (Constr.mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> match reconsider_unif_constraints (evar_conv_x ts) evd with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> evd else @@ -1270,7 +1270,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | None -> evd | Some (evk,ev_info,l) -> let rec aux = function - | [] -> error "Unsolvable existential variables." + | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> try let conv_algo = evar_conv_x ts in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4ada91eb5..98e71c7fd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1050,7 +1050,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = | None -> None,candidates | Some filter -> restrict_hyps evd evk filter candidates in match candidates,filter with - | UpdateWith [], _ -> error "Not solvable." + | UpdateWith [], _ -> user_err Pp.(str "Not solvable.") | UpdateWith [nc],_ -> let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) @@ -1230,7 +1230,7 @@ let check_evar_instance evd evk1 body conv_algo = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> error "Ill-typed evar instance" + with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") in match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with | Success evd -> evd diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 429e5005e..7f3bafc68 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -97,7 +97,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and ntypes = mib.mind_ntypes and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in - if j > nconstr then error "Not enough constructors in the type."; + if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) (* Number of constructors *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index e4fbf8d54..211ffbe01 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -50,9 +50,9 @@ let is_nowhere = function let simple_clause_of enum_hyps cl = let error_occurrences () = - CErrors.error "This tactic does not support occurrences selection" in + CErrors.user_err Pp.(str "This tactic does not support occurrences selection") in let error_body_selection () = - CErrors.error "This tactic does not support body selection" in + CErrors.user_err Pp.(str "This tactic does not support body selection") in let hyps = match cl.onhyps with | None -> diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0228f63cd..afaa20b6f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -383,7 +383,7 @@ let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in if Coq_config.no_native_compiler then - error "Native_compute reduction has been disabled at configure time." + user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else let penv = Environ.pre_env env in (* diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a8012d35f..1c8ad0cdd 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -230,7 +230,7 @@ let instantiate_pattern env sigma lvar c = error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) - | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") + | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.") | c -> map_pattern_with_binders (fun id vars -> id::vars) aux vars c in aux [] c diff --git a/pretyping/redops.ml b/pretyping/redops.ml index 7d65925e5..8e190f40b 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -20,13 +20,13 @@ let make_red_flag l = | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l; rDelta = true } lf diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 117ed338e..e7c963582 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1219,7 +1219,7 @@ let clos_norm_flags flgs env sigma t = EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let clos_whd_flags flgs env sigma t = try @@ -1227,7 +1227,7 @@ let clos_whd_flags flgs env sigma t = EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 67221046b..3d41d2ddd 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -858,7 +858,7 @@ let try_red_product env sigma c = let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "No head constant to reduce." + with Redelimination -> user_err (str "No head constant to reduce.") (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -1080,7 +1080,7 @@ let unfold env sigma name c = if is_evaluable env name then clos_norm_flags (unfold_red name) env sigma c else - error (string_of_evaluable_ref env name^" is opaque.") + user_err Pp.(str (string_of_evaluable_ref env name^" is opaque.")) (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. @@ -1090,7 +1090,7 @@ let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in if Int.equal nbocc 1 then - error ((string_of_evaluable_ref env name)^" does not occur."); + user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur.")); let rest = List.filter (fun o -> o >= nbocc) locs in let () = match rest with | [] -> () @@ -1112,7 +1112,7 @@ let unfoldn loccname env sigma c = let fold_one_com com env sigma c = let rcom = try red_product env sigma com - with Redelimination -> error "Not reducible." in + with Redelimination -> user_err Pp.(str "Not reducible.") in (* Reason first on the beta-iota-zeta normal form of the constant as unfold produces it, so that the "unfold f; fold f" configuration works to refold fix expressions *) @@ -1147,7 +1147,7 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in let na = named_hd env sigma ta Anonymous in - if occur_meta sigma ta then error "Cannot find a type for the generalisation."; + if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation."); if occur_meta sigma a then mkLambda (na,ta,c), sigma else diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 919e95a8e..d7b484281 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -422,7 +422,7 @@ let add_class cl = match inst with | Some (Backward, info) -> (match body with - | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") | Some b -> declare_instance (Some info) false (ConstRef b)) | _ -> ()) cl.cl_projs diff --git a/pretyping/unification.ml b/pretyping/unification.ml index cac6c5057..d1643a8c7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1250,7 +1250,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = | Prod (_,c1,c2) -> let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' - | _ -> error "Apply_Head_Then" + | _ -> user_err Pp.(str "Apply_Head_Then") in apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd @@ -1516,7 +1516,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 = let iter_fail f a = let n = Array.length a in let rec ffail i = - if Int.equal i n then error "iter_fail" + if Int.equal i n then user_err Pp.(str "iter_fail") else try f a.(i) with ex when precatchable_exception ex -> ffail (i+1) @@ -1754,8 +1754,8 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = w_typed_unify_array env evd flags f1 l1 f2 l2,cl else w_typed_unify env evd CONV flags op cl,cl with ex when Pretype_errors.unsatisfiable_exception ex -> - bestexn := Some ex; error "Unsat") - else error "Bound 1" + bestexn := Some ex; user_err Pp.(str "Unsat")) + else user_err Pp.(str "Bound 1") with ex when precatchable_exception ex -> (match EConstr.kind evd cl with | App (f,args) -> @@ -1804,7 +1804,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = with ex when precatchable_exception ex -> matchrec c) - | _ -> error "Match_subterm")) + | _ -> user_err Pp.(str "Match_subterm"))) in try matchrec cl with ex when precatchable_exception ex -> @@ -1820,7 +1820,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = let (evd,c as a) = a () in if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b in - let fail str _ = error str in + let fail str _ = user_err (Pp.str str) in let bind f g a = let a1 = try f a with ex @@ -1956,7 +1956,7 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 = | _, Meta p2 -> (* Find the predicate *) secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2) - | _ -> error "w_unify2" + | _ -> user_err Pp.(str "w_unify2") (* The unique unification algorithm works like this: If the pattern is flexible, and the goal has a lambda-abstraction at the head, then diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 74998349b..b08666483 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -355,7 +355,7 @@ and nf_cofix env sigma cf = let cbv_vm env sigma c t = if Termops.occur_meta_or_existential sigma c then - CErrors.error "vm_compute does not support existential variables."; + CErrors.user_err Pp.(str "vm_compute does not support existential variables."); (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr sigma c in let t = EConstr.to_constr sigma t in diff --git a/printing/pputils.ml b/printing/pputils.ml index d1ba1a4a1..99d07601c 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -96,7 +96,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) | Red true -> - CErrors.error "Shouldn't be accessible from user." + CErrors.user_err Pp.(str "Shouldn't be accessible from user.") | ExtraRedExpr s -> str s | CbvVm o -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 70de65acd..0f7da3613 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -716,7 +716,7 @@ let read_sec_context r = | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | (_,Lib.ClosedSection _)::rest -> - error "Cannot print the contents of a closed section." + user_err Pp.(str "Cannot print the contents of a closed section.") (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest @@ -765,7 +765,7 @@ let print_opaque_name qid = if Declareops.constant_has_body cb then print_constant_with_infos cst else - error "Not a defined constant." + user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> diff --git a/printing/printer.ml b/printing/printer.ml index d4f7afb38..ebe68680f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -566,7 +566,7 @@ let pr_selected_subgoal name sigma g = let default_pr_subgoal n sigma = let rec prrec p = function - | [] -> error "No such goal." + | [] -> user_err Pp.(str "No such goal.") | g::rest -> if Int.equal p 1 then pr_selected_subgoal (int n) sigma g @@ -828,7 +828,7 @@ let pr_goal_by_id id = Proof.in_proof p (fun sigma -> let g = Evd.evar_key id sigma in pr_selected_subgoal (pr_id id) sigma g) - with Not_found -> error "No such goal." + with Not_found -> user_err Pp.(str "No such goal.") let pr_goal_by_uid uid = let p = Proof_global.give_me_the_proof () in @@ -839,7 +839,7 @@ let pr_goal_by_uid uid = in try Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;}) - with Not_found -> error "Invalid goal identifier." + with Not_found -> user_err Pp.(str "Invalid goal identifier.") (* Elementary tactics *) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9e0a2a03e..33a86402e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -163,7 +163,7 @@ let error_incompatible_inst clenv mv = let clenv_assign mv rhs clenv = let rhs_fls = mk_freelisted rhs in if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then - error "clenv_assign: circularity in unification"; + user_err Pp.(str "clenv_assign: circularity in unification"); try if meta_defined clenv.evd mv then if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then @@ -174,7 +174,7 @@ let clenv_assign mv rhs clenv = let st = (Conv,TypeNotProcessed) in {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} with Not_found -> - error "clenv_assign: undefined meta" + user_err Pp.(str "clenv_assign: undefined meta") diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index b9c925796..b1fe128a2 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -39,11 +39,11 @@ let define_and_solve_constraints evk c env evd = pbs with | Success evd -> evd - | UnifFailure _ -> error "Instance does not satisfy the constraints." + | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.") let w_refine (evk,evi) (ltac_var,rawc) sigma = if Evd.is_defined sigma evk then - error "Instantiate called on already-defined evar"; + user_err Pp.(str "Instantiate called on already-defined evar"); let env = Evd.evar_filtered_env evi in let sigma',typed_c = let flags = { diff --git a/proofs/logic.ml b/proofs/logic.ml index 54345abd9..cd2cfbd32 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -141,7 +141,7 @@ let occur_vars_in_decl env sigma hyps d = let reorder_context env sigma sign ord = let ords = List.fold_right Id.Set.add ord Id.Set.empty in if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then - error "Order list has duplicates"; + user_err Pp.(str "Order list has duplicates"); let rec step ord expected ctxt_head moved_hyps ctxt_tail = match ord with | [] -> List.rev ctxt_tail @ ctxt_head diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 92b4e788a..aaceb7b76 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -71,7 +71,7 @@ let get_universe_binders () = exception NoSuchGoal let _ = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.error "No such goal." + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end let get_nth_V82_goal i = @@ -87,12 +87,12 @@ let get_goal_context_gen i = let get_goal_context i = try get_goal_context_gen i - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." - | NoSuchGoal -> CErrors.error "No such goal." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") + | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") let get_current_goal_context () = try get_goal_context_gen 1 - with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) @@ -143,7 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) with - Proof_global.NoCurrentProof -> CErrors.error "No focused proof" + Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) diff --git a/proofs/proof.ml b/proofs/proof.ml index b2103489a..2aa620c1d 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -66,14 +66,14 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - CErrors.error "This proof is focused, but cannot be unfocused this way" + CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") | NoSuchGoals (i,j) when Int.equal i j -> CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) - | FullyUnfocused -> CErrors.error "The proof is not focused" + | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -301,10 +301,10 @@ exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar let _ = CErrors.register_handler begin function - | UnfinishedProof -> CErrors.error "Some goals have not been solved." - | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf." - | HasGivenUpGoals -> CErrors.error "Some goals have been given up." - | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated." + | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.") + | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.") + | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.") + | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.") | _ -> raise CErrors.Unhandled end @@ -420,9 +420,9 @@ module V82 = struct let evl = Evarutil.non_instantiated sigma in let evl = Evar.Map.bindings evl in if (n <= 0) then - CErrors.error "incorrect existential variable index" + CErrors.user_err Pp.(str "incorrect existential variable index") else if CList.length evl < n then - CErrors.error "not so many uninstantiated existential variables" + CErrors.user_err Pp.(str "not so many uninstantiated existential variables") else CList.nth evl (n-1) in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 95aee72cb..4d2f534a7 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -36,7 +36,7 @@ let proof_modes = Hashtbl.create 6 let find_proof_mode n = try Hashtbl.find proof_modes n with Not_found -> - CErrors.error (Format.sprintf "No proof mode named \"%s\"." n) + CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) let register_proof_mode ({name = n} as m) = Hashtbl.add proof_modes n (CEphemeron.create m) @@ -124,13 +124,13 @@ let push a l = l := a::!l; exception NoSuchProof let _ = CErrors.register_handler begin function - | NoSuchProof -> CErrors.error "No such proof." + | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") | _ -> raise CErrors.Unhandled end exception NoCurrentProof let _ = CErrors.register_handler begin function - | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)." + | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -299,7 +299,7 @@ let set_used_variables l = | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then - CErrors.error "Used section variables can be declared only once"; + CErrors.user_err Pp.(str "Used section variables can be declared only once"); pstates := { p with section_vars = Some ctx} :: rest; ctx, to_clear @@ -637,7 +637,7 @@ module Bullet = struct current_behavior := try Hashtbl.find behaviors n with Not_found -> - CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") + CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) end }) @@ -687,9 +687,9 @@ let parse_goal_selector = function let err_msg = "The default selector must be \"all\" or a natural number." in begin try let i = int_of_string i in - if i < 0 then CErrors.error err_msg; + if i < 0 then CErrors.user_err Pp.(str err_msg); Vernacexpr.SelectNth i - with Failure _ -> CErrors.error err_msg + with Failure _ -> CErrors.user_err Pp.(str err_msg) end let _ = diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index b2ea3341b..9f50ab589 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -24,7 +24,7 @@ end module Pool = Map.Make(IntOT) let schedule_vio_checking j fs = - if j < 1 then CErrors.error "The number of workers must be bigger than 0"; + if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun f -> let f = @@ -98,7 +98,7 @@ let schedule_vio_checking j fs = exit !rc let schedule_vio_compilation j fs = - if j < 1 then CErrors.error "The number of workers must be bigger than 0"; + if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun f -> let f = diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 918371d55..46d66b9d0 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -938,7 +938,7 @@ module V85 = struct | Some (evd', fk) -> if unique then (match get_result (fk NotApplicable) with - | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions" + | Some (evd'', fk') -> user_err Pp.(str "Typeclass resolution gives multiple solutions") | None -> evd') else evd' diff --git a/tactics/eauto.ml b/tactics/eauto.ml index e87368dec..986f53139 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -62,7 +62,7 @@ let registered_e_assumption = let first_goal gls = let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in - if List.is_empty gl then error "first_goal"; + if List.is_empty gl then user_err Pp.(str "first_goal"); { Evd.it = List.hd gl; Evd.sigma = sig_0; } (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) @@ -73,7 +73,7 @@ let apply_tac_list tac glls = | (g1::rest) -> let gl = apply_sig_tac sigr tac g1 in repackage sigr (gl@rest) - | _ -> error "apply_tac_list" + | _ -> user_err Pp.(str "apply_tac_list") let one_step l gl = [Proofview.V82.of_tactic Tactics.intro] @@ -82,7 +82,7 @@ let one_step l gl = @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl)) let rec prolog l n gl = - if n <= 0 then error "prolog - failure"; + if n <= 0 then user_err Pp.(str "prolog - failure"); let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl @@ -402,7 +402,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl = s.tacres with Not_found -> pr_info_nop d; - error "eauto: search failed" + user_err Pp.(str "eauto: search failed") (* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) (* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index d023b4568..bcd31cb7e 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -103,7 +103,7 @@ let get_coq_eq ctx = (Universes.fresh_inductive_instance (Global.env ()) eq) in mkIndU eq, mkConstructUi (eq,1), ctx with Not_found -> - error "eq not found." + user_err Pp.(str "eq not found.") let univ_of_eq env eq = let eq = EConstr.of_constr eq in @@ -120,6 +120,8 @@ let univ_of_eq env eq = (* in which case, a symmetry lemma is definable *) (**********************************************************************) +let error msg = user_err Pp.(str msg) + let get_sym_eq_data env (ind,u) = let (mib,mip as specif) = lookup_mind_specif env ind in if not (Int.equal (Array.length mib.mind_packets) 1) || diff --git a/tactics/equality.ml b/tactics/equality.ml index 0a68ff129..e6278943d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -164,7 +164,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in let arglen = Array.length args in - let () = if arglen < 2 then error "The term provided is not an applied relation." in + let () = if arglen < 2 then user_err Pp.(str "The term provided is not an applied relation.") in let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = @@ -441,7 +441,7 @@ let adjust_rewriting_direction args lft2rgt = (* equality to a constant, like in eq_true *) (* more natural to see -> as the rewriting to the constant *) if not lft2rgt then - error "Rewriting non-symmetric equality not allowed from right-to-left."; + user_err Pp.(str "Rewriting non-symmetric equality not allowed from right-to-left."); None | _ -> (* other equality *) @@ -865,7 +865,7 @@ let descend_then env sigma head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> - error "Cannot project on an inductive type derived from a dependency." in + user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in let indp,_ = (dest_ind_family indf) in let ind, _ = check_privacy env indp in let (mib,mip) = lookup_mind_specif env ind in @@ -1202,7 +1202,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in dflt with Evarconv.UnableToUnify _ -> - error "Cannot solve a unification problem." + user_err Pp.(str "Cannot solve a unification problem.") else let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with | (_sigS,[a;p]) -> (a, p) @@ -1219,7 +1219,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let exist_term = EConstr.of_constr exist_term in applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) else - error "Cannot solve a unification problem." + user_err Pp.(str "Cannot solve a unification problem.") | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; @@ -1227,7 +1227,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = tried in the first place in make_iterated_tuple instead of approximatively computing the free rels; then unsolved evars would mean not binding rel *) - error "Cannot solve a unification problem." + user_err Pp.(str "Cannot solve a unification problem.") in let scf = sigrec_clausal_form siglen ty in !evdref, Evarutil.nf_evar !evdref scf @@ -1886,7 +1886,7 @@ let cond_eq_term c t gl = let rewrite_assumption_cond cond_eq_term cl = let rec arec hyps gl = match hyps with - | [] -> error "No such assumption." + | [] -> user_err Pp.(str "No such assumption.") | hyp ::rest -> let id = NamedDecl.get_id hyp in begin diff --git a/tactics/hints.ml b/tactics/hints.ml index e6edae7ef..48a7b3f75 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -59,7 +59,7 @@ let head_constr_bound sigma t = | _ -> raise Bound let head_constr sigma c = - try head_constr_bound sigma c with Bound -> error "Bound head variable." + try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.") let decompose_app_bound sigma t = let t = strip_outer_cast sigma t in @@ -167,7 +167,7 @@ let write_warn_hint = function | "Lax" -> warn_hint := `LAX | "Warn" -> warn_hint := `WARN | "Strict" -> warn_hint := `STRICT -| _ -> error "Only the following flags are accepted: Lax, Warn, Strict." +| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") let _ = Goptions.declare_string_option @@ -767,7 +767,7 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with let try_head_pattern c = try head_pattern_bound c - with BoundPattern -> error "Bound head variable." + with BoundPattern -> user_err Pp.(str "Bound head variable.") let with_uid c = { obj = c; uid = fresh_key () } @@ -980,8 +980,8 @@ let get_db dbname = let add_hint dbname hintlist = let check (_, h) = let () = if KNmap.mem h.code.uid !statustable then - error "Conflicting hint keys. This can happen when including \ - twice the same module." + user_err Pp.(str "Conflicting hint keys. This can happen when including \ + twice the same module.") in statustable := KNmap.add h.code.uid false !statustable in @@ -1246,10 +1246,10 @@ let prepare_hint check (poly,local) env init (sigma,c) = let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in if not (closed0 sigma c) then - error "Hints with holes dependent on a bound variable not supported."; + user_err Pp.(str "Hints with holes dependent on a bound variable not supported."); if occur_existential sigma t then (* Not clever enough to construct dependency graph of evars *) - error "Not clever enough to deal with evars dependent in other evars."; + user_err Pp.(str "Not clever enough to deal with evars dependent in other evars."); raise (Found (c,t)) | _ -> EConstr.iter sigma find_next_evar c in let rec iter c = @@ -1322,7 +1322,7 @@ let interp_hints poly = let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then - error "The hint database \"nocore\" is meant to stay empty."; + user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in let env = Global.env() in let sigma = Evd.from_env env in @@ -1471,7 +1471,7 @@ let pr_applicable_hint () = let pts = get_pftreestate () in let glss = Proof.V82.subgoals pts in match glss.Evd.it with - | [] -> CErrors.error "No focused goal." + | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index dce98eed7..fd5eabe64 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -460,7 +460,7 @@ let find_this_eq_data_decompose gl eqn = let eq_args = try extract_eq_args gl eq_args with PatternMatchingFailure -> - error "Don't know what to do with JMeq on arguments not of same type." in + user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) let match_eq_nf gls eqn (ref, hetero) = @@ -477,7 +477,7 @@ let dest_nf_eq gls eqn = try snd (first_match (match_eq_nf gls eqn) equalities) with PatternMatchingFailure -> - error "Not an equality." + user_err Pp.(str "Not an equality.") (*** Sigma-types *) diff --git a/tactics/inv.ml b/tactics/inv.ml index 5c4b73a62..b951e7ceb 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -292,27 +292,27 @@ let error_too_many_names pats = let get_names (allow_conj,issimple) (loc, pat as x) = match pat with | IntroNaming IntroAnonymous | IntroForthcoming _ -> - error "Anonymous pattern not allowed for inversion equations." + user_err Pp.(str "Anonymous pattern not allowed for inversion equations.") | IntroNaming (IntroFresh _) -> - error "Fresh pattern not allowed for inversion equations." + user_err Pp.(str "Fresh pattern not allowed for inversion equations.") | IntroAction IntroWildcard -> - error "Discarding pattern not allowed for inversion equations." + user_err Pp.(str "Discarding pattern not allowed for inversion equations.") | IntroAction (IntroRewrite _) -> - error "Rewriting pattern not allowed for inversion equations." + user_err Pp.(str "Rewriting pattern not allowed for inversion equations.") | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, []) | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ])) when allow_conj -> (Some id,l) | IntroAction (IntroOrAndPattern (IntroAndPattern _)) -> if issimple then - error"Conjunctive patterns not allowed for simple inversion equations." + user_err Pp.(str"Conjunctive patterns not allowed for simple inversion equations.") else - error"Nested conjunctive patterns not allowed for inversion equations." + user_err Pp.(str"Nested conjunctive patterns not allowed for inversion equations.") | IntroAction (IntroInjection l) -> - error "Injection patterns not allowed for inversion equations." + user_err Pp.(str "Injection patterns not allowed for inversion equations.") | IntroAction (IntroOrAndPattern (IntroOrPattern _)) -> - error "Disjunctive patterns not allowed for inversion equations." + user_err Pp.(str "Disjunctive patterns not allowed for inversion equations.") | IntroAction (IntroApplyOn (c,pat)) -> - error "Apply patterns not allowed for inversion equations." + user_err Pp.(str "Apply patterns not allowed for inversion equations.") | IntroNaming (IntroIdentifier id) -> (Some id,[x]) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fe9cb123c..c495b5ece 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -69,7 +69,7 @@ let tclTHENSEQ = tclTHENLIST let nthDecl m gl = try List.nth (pf_hyps gl) (m-1) - with Failure _ -> error "No such assumption." + with Failure _ -> user_err Pp.(str "No such assumption.") let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -80,7 +80,7 @@ let lastHyp gl = nthHyp 1 gl let nLastDecls n gl = try List.firstn n (pf_hyps gl) - with Failure _ -> error "Not enough hypotheses in the goal." + with Failure _ -> user_err Pp.(str "Not enough hypotheses in the goal.") let nLastHypsId n gl = List.map (NamedDecl.get_id) (nLastDecls n gl) let nLastHyps n gl = List.map mkVar (nLastHypsId n gl) @@ -533,11 +533,11 @@ module New = struct let hyps = Proofview.Goal.hyps gl in try List.nth hyps (m-1) - with Failure _ -> CErrors.error "No such assumption." + with Failure _ -> CErrors.user_err Pp.(str "No such assumption.") let nLastDecls gl n = try List.firstn n (Proofview.Goal.hyps gl) - with Failure _ -> error "Not enough hypotheses in the goal." + with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.") let nthHypId m gl = (** We only use [id] *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 617d3d701..7e8cb4e63 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -195,6 +195,7 @@ let introduction ?(check=true) id = end } let refine = Tacmach.refine +let error msg = CErrors.user_err Pp.(str msg) let convert_concl ?(check=true) ty k = Proofview.Goal.enter { enter = begin fun gl -> diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 930b092d3..044399544 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -495,7 +495,7 @@ let coqdep () = add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 7fa8fd58d..defc80338 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -227,7 +227,7 @@ let declare_loading_string () = \n Mltop.set_top\ \n {Mltop.load_obj=\ \n (fun f -> if not (Topdirs.load_file ppf f)\ -\n then CErrors.error (\"Could not load plugin \"^f));\ +\n then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\ \n Mltop.use_file=Topdirs.dir_use ppf;\ \n Mltop.add_dir=Topdirs.dir_directory;\ \n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ @@ -257,7 +257,7 @@ let create_tmp_main_file modules = let main () = let (options, userfiles) = parse_args () in (* Directories: *) - let () = Envars.set_coqlib ~fail:CErrors.error in + let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in (* Which ocaml compiler to invoke *) let prog = if !opt then "opt" else "ocamlc" in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ac1e623d7..7834b5113 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -133,7 +133,7 @@ let set_batch_mode () = batch_mode := true let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) let toplevel_name = ref toplevel_default_name let set_toplevel_name dir = - if Names.DirPath.is_empty dir then error "Need a non empty toplevel module name"; + if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); toplevel_name := dir let remove_top_ml () = Mltop.remove () @@ -245,7 +245,7 @@ let compile_files () = let set_emacs () = if not (Option.is_empty !toploop) then - error "Flag -emacs is incompatible with a custom toplevel loop"; + user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); Flags.print_emacs := true; Printer.enable_goal_tags_printing := true; color := `OFF @@ -253,14 +253,14 @@ let set_emacs () = (** Options for CoqIDE *) let set_ideslave () = - if !Flags.print_emacs then error "Flags -ideslave and -emacs are incompatible"; + if !Flags.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); toploop := Some "coqidetop"; Flags.ide_slave := true (** Options for slaves *) let set_toploop name = - if !Flags.print_emacs then error "Flags -toploop and -emacs are incompatible"; + if !Flags.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible"); toploop := Some name (** GC tweaking *) @@ -591,7 +591,7 @@ let parse_args arglist = |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml () |"-emacs-U" -> warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () - |"-v7" -> error "This version of Coq does not support v7 syntax" + |"-v7" -> user_err Pp.(str "This version of Coq does not support v7 syntax") |"-v8" -> warning "Obsolete option \"-v8\"." |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"." |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"." @@ -619,7 +619,7 @@ let init_toplevel arglist = (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); if !print_config then (Envars.print_config stdout; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7e81aa20a..a61ade784 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -29,7 +29,7 @@ let checknav_deep (loc, ast) = let disable_drop = function - | Drop -> CErrors.error "Drop is forbidden." + | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.") | e -> e (* Echo from a buffer based on position. diff --git a/vernac/classes.ml b/vernac/classes.ml index 5843da31e..004083dcf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -353,7 +353,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) (); id) end - else CErrors.error "Unsolved obligations remaining.") + else CErrors.user_err Pp.(str "Unsolved obligations remaining.")) let named_of_rel_context l = let acc, ctx = @@ -379,7 +379,7 @@ let context poly l = let ctx = try named_of_rel_context fullctx with e when CErrors.noncritical e -> - error "Anonymous variables not allowed in contexts." + user_err Pp.(str "Anonymous variables not allowed in contexts.") in let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = diff --git a/vernac/command.ml b/vernac/command.ml index 9382da3fb..e2ebb4d7f 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -382,7 +382,7 @@ type structured_inductive_expr = local_binder_expr list * structured_one_inductive_expr list let minductive_message warn = function - | [] -> error "No inductive definition." + | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (pr_id x ++ str " is defined" ++ if warn then str " as a non-primitive record" else mt()) | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -676,8 +676,8 @@ let extract_params indl = match paramsl with | [] -> anomaly (Pp.str "empty list of inductive types") | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then error - "Parameters should be syntactically the same for each inductive type."; + if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str + "Parameters should be syntactically the same for each inductive type."); params let extract_inductive indl = @@ -715,9 +715,9 @@ let declare_mutual_inductive_with_eliminations mie pl impls = begin match mie.mind_entry_finite with | BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then - error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." + user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") else - error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.") + user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) | _ -> () end; let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in @@ -1123,7 +1123,7 @@ let interp_recursive isfix fixl notations = | x , None -> x | Some ls , Some us -> if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then - error "(co)-recursive definitions should all have the same universe binders"; + user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in let ctx = Evd.make_evar_universe_context env all_universes in let evdref = ref (Evd.from_ctx ctx) in @@ -1263,8 +1263,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let extract_decreasing_argument limit = function | (na,CStructRec) -> na | (na,_) when not limit -> na - | _ -> error - "Only structural decreasing is supported for a non-Program Fixpoint" + | _ -> user_err Pp.(str + "Only structural decreasing is supported for a non-Program Fixpoint") let extract_fixpoint_components limit l = let fixl, ntnl = List.split l in @@ -1283,7 +1283,7 @@ let extract_cofixpoint_components l = let out_def = function | Some def -> def - | None -> error "Program Fixpoint needs defined bodies." + | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml index c6588684a..f3259f1f3 100644 --- a/vernac/ind_tables.ml +++ b/vernac/ind_tables.ml @@ -81,7 +81,7 @@ let scheme_object_table = let declare_scheme_object s aux f = let () = if not (Id.is_valid ("ind" ^ s)) then - error ("Illegal induction scheme suffix: " ^ s) + user_err Pp.(str ("Illegal induction scheme suffix: " ^ s)) in let key = if String.is_empty aux then s else aux in try diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 885769143..f57b1bba0 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -418,7 +418,7 @@ let get_common_underlying_mutual_inductive = function raise (RecursionSchemeError (NotMutualInScheme (ind,ind'))) | [] -> if not (List.distinct_f Int.compare (List.map snd (List.map snd all))) - then error "A type occurs twice"; + then user_err Pp.(str "A type occurs twice"); mind, List.map_filter (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all @@ -429,7 +429,7 @@ let do_scheme l = tried to declare different schemes at once *) if not (List.is_empty ischeme) && not (List.is_empty escheme) then - error "Do not declare equality and induction scheme at the same time." + user_err Pp.(str "Do not declare equality and induction scheme at the same time.") else ( if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme else @@ -498,7 +498,7 @@ let do_combined_scheme name schemes = let refe = Ident x in let qualid = qualid_of_reference refe in try Nametab.locate_constant (snd qualid) - with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")) + with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) schemes in let body,typ = build_combined_scheme (Global.env ()) csts in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index c67a3302f..d6ae0ea86 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -153,9 +153,9 @@ let find_mutually_recursive_statements thms = (* assume the largest indices as possible *) List.last common_same_indhyp, false, possible_guards | _, [] -> - error + user_err Pp.(str ("Cannot find common (mutual) inductive premises or coinductive" ^ - " conclusions in the statements.") + " conclusions in the statements.")) in (finite,guard,None), ordered_inds @@ -273,7 +273,7 @@ let save_named ?export_seff proof = let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then - error "This command can only be used for unnamed theorem." + user_err Pp.(str "This command can only be used for unnamed theorem.") let save_anonymous ?export_seff proof save_ident = let id,const,(cstrs,pl),do_guard,persistence,hook = proof in @@ -478,10 +478,10 @@ let save_proof ?proof = function match proof with | Some ({ id; entries; persistence = k; universes }, _) -> if List.length entries <> 1 then - error "Admitted does not support multiple statements"; + user_err Pp.(str "Admitted does not support multiple statements"); let { const_entry_secctx; const_entry_type } = List.hd entries in if const_entry_type = None then - error "Admitted requires an explicit statement"; + user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in diff --git a/vernac/locality.ml b/vernac/locality.ml index 03640676e..a25acb0d3 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -35,9 +35,9 @@ let enforce_locality_full locality_flag local = let local = match locality_flag with | Some false when local -> - CErrors.error "Cannot be simultaneously Local and Global." + CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.") | Some true when local -> - CErrors.error "Use only prefix \"Local\"." + CErrors.user_err Pp.(str "Use only prefix \"Local\".") | None -> if local then begin warn_deprecated_local_syntax (); @@ -66,7 +66,7 @@ let enforce_locality_exp locality_flag local = | None, Some local -> local | Some b, None -> local_of_bool b | None, None -> Decl_kinds.Global - | Some _, Some _ -> CErrors.error "Local non allowed in this case" + | Some _, Some _ -> CErrors.user_err Pp.(str "Local non allowed in this case") (* For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; @@ -87,8 +87,8 @@ let enforce_section_locality locality_flag local = let make_module_locality = function | Some false -> if Lib.sections_are_opened () then - CErrors.error - "This command does not support the Global option in sections."; + CErrors.user_err Pp.(str + "This command does not support the Global option in sections."); false | Some true -> true | None -> false diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index fb7c72941..42494dd28 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -60,7 +60,7 @@ let pr_entry e = let pr_registered_grammar name = let gram = try Some (String.Map.find name !grammars) with Not_found -> None in match gram with - | None -> error "Unknown or unprintable grammar entry." + | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") | Some entries -> let pr_one (AnyEntry e) = str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++ @@ -107,11 +107,11 @@ let parse_format ((loc, str) : lstring) = if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in let close_box i b = function | a::(_::_ as l) -> push_token (UnpBox (b,a)) l - | _ -> error "Non terminated box in format." in + | _ -> user_err Pp.(str "Non terminated box in format.") in let close_quotation i = if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ') then i+1 - else error "Incorrectly terminated quoted expression." in + else user_err Pp.(str "Incorrectly terminated quoted expression.") in let rec spaces n i = if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1) else n in @@ -119,10 +119,10 @@ let parse_format ((loc, str) : lstring) = if i < String.length str && str.[i] != ' ' then if str.[i] == '\'' && quoted && (i+1 >= String.length str || str.[i+1] == ' ') - then if Int.equal n 0 then error "Empty quoted token." else n + then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n else nonspaces quoted (n+1) (i+1) else - if quoted then error "Spaces are not allowed in (quoted) symbols." + if quoted then user_err Pp.(str "Spaces are not allowed in (quoted) symbols.") else n in let rec parse_non_format i = let n = nonspaces false 0 i in @@ -153,8 +153,8 @@ let parse_format ((loc, str) : lstring) = (* Parse " [ .. ", *) | ' ' | '\'' -> parse_box (fun n -> PpHOVB n) (i+1) - | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format." - else error "\"v\", \"hv\" or \" \" expected after \"[\" in format." + | _ -> user_err Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.") + else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.") (* Parse "]" *) | ']' -> ([] :: parse_token (close_quotation (i+1))) @@ -165,7 +165,7 @@ let parse_format ((loc, str) : lstring) = (parse_token (close_quotation (i+n)))) else if Int.equal n 0 then [] - else error "Ending spaces non part of a format annotation." + else user_err Pp.(str "Ending spaces non part of a format annotation.") and parse_box box i = let n = spaces 0 i in close_box i (box n) (parse_token (close_quotation (i+n))) @@ -187,9 +187,9 @@ let parse_format ((loc, str) : lstring) = try if not (String.is_empty str) then match parse_token 0 with | [l] -> l - | _ -> error "Box closed without being opened in format." + | _ -> user_err Pp.(str "Box closed without being opened in format.") else - error "Empty format." + user_err Pp.(str "Empty format.") with reraise -> let (e, info) = CErrors.push reraise in let info = Option.cata (Loc.add_loc info) info loc in @@ -243,19 +243,19 @@ let rec find_pattern nt xl = function | [], NonTerminal x' :: l' -> (out_nt nt,x',List.rev xl),l' | _, Break s :: _ | Break s :: _, _ -> - error ("A break occurs on one side of \"..\" but not on the other side.") + user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side.")) | _, Terminal s :: _ | Terminal s :: _, _ -> user_err ~hdr:"Metasyntax.find_pattern" (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") | _, [] -> - error msg_expected_form_of_recursive_notation + user_err Pp.(str msg_expected_form_of_recursive_notation) | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right") let rec interp_list_parser hd = function | [] -> [], List.rev hd | NonTerminal id :: tl when Id.equal id ldots_var -> - if List.is_empty hd then error msg_expected_form_of_recursive_notation; + if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation); let hd = List.rev hd in let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in let xyl,tl'' = interp_list_parser [] tl' in @@ -286,7 +286,7 @@ let quote_notation_token x = let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl - | String "_" :: _ -> error "_ must be quoted." + | String "_" :: _ -> user_err Pp.(str "_ must be quoted.") | String x :: sl when CLexer.is_ident x -> NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> @@ -487,7 +487,7 @@ let make_hunks etyps symbols from = (* Build default printing rules from explicit format *) -let error_format () = error "The format does not match the notation." +let error_format () = user_err Pp.(str "The format does not match the notation.") let rec split_format_at_ldots hd = function | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt @@ -500,7 +500,7 @@ and check_no_ldots_in_box = function | UnpBox (_,fmt) -> (try let _ = split_format_at_ldots [] fmt in - error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.") + user_err Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")) with Exit -> ()) | _ -> () @@ -518,7 +518,7 @@ let read_recursive_format sl fmt = let rec get_tail = function | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail - | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in + | _ -> user_err Pp.(str "The format is not the same on the right and left hand side of the special token \"..\".") in let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) @@ -652,7 +652,7 @@ let make_production etyps symbols = distribute [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll | _ -> - error "Components of recursive patterns in notation must be terms or binders.") + user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.")) symbols [[]] in List.map define_keywords prod @@ -811,7 +811,7 @@ let interp_modifiers modl = let open NotationMods in interp { acc with level = Some n; } l | SetAssoc a :: l -> - if not (Option.is_empty acc.assoc) then error "An associativity is given more than once."; + if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once."); interp { acc with assoc = Some a; } l | SetOnlyParsing :: l -> interp { acc with only_parsing = true; } l @@ -820,7 +820,7 @@ let interp_modifiers modl = let open NotationMods in | SetCompatVersion v :: l -> interp { acc with compat = Some v; } l | SetFormat ("text",s) :: l -> - if not (Option.is_empty acc.format) then error "A format is given more than once."; + if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once."); interp { acc with format = Some s; } l | SetFormat (k,(_,s)) :: l -> interp { acc with extra = (k,s)::acc.extra; } l @@ -829,7 +829,7 @@ let interp_modifiers modl = let open NotationMods in let check_infix_modifiers modifiers = let t = (interp_modifiers modifiers).NotationMods.etyps in if not (List.is_empty t) then - error "Explicit entry level or type unexpected in infix notation." + user_err Pp.(str "Explicit entry level or type unexpected in infix notation.") let check_useless_entry_types recvars mainvars etyps = let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in @@ -901,7 +901,7 @@ let internalization_type_of_entry_type = function | ETBigint | ETReference -> NtnInternTypeConstr | ETBinder _ -> NtnInternTypeBinder | ETName -> NtnInternTypeIdent - | ETPattern | ETOther _ -> error "Not supported." + | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.") | ETBinderList _ | ETConstrList _ -> assert false let set_internalization_type typs = @@ -917,7 +917,7 @@ let make_interpretation_type isrec isonlybinding = function | NtnInternTypeConstr | NtnInternTypeIdent -> if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." + | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.") let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = @@ -938,9 +938,9 @@ let make_interpretation_vars recvars allvars = let check_rule_productivity l = if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then - error "A notation must include at least one symbol."; + user_err Pp.(str "A notation must include at least one symbol."); if (match l with SProdList _ :: _ -> true | _ -> false) then - error "A recursive notation must start with at least one symbol." + user_err Pp.(str "A recursive notation must start with at least one symbol.") let warn_notation_bound_to_variable = CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing" @@ -980,7 +980,7 @@ let find_precedence lev etyps symbols = | Some (NonTerminal x) -> (try match List.assoc x etyps with | ETConstr _ -> - error "The level of the leftmost non-terminal cannot be changed." + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") | ETName | ETBigint | ETReference -> begin match lev with | None -> @@ -988,31 +988,31 @@ let find_precedence lev etyps symbols = | Some 0 -> ([],0) | _ -> - error "A notation starting with an atomic expression must be at level 0." + user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") end | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *) if Option.is_empty lev then - error "Need an explicit level." + user_err Pp.(str "Need an explicit level.") else [],Option.get lev | ETConstrList _ | ETBinderList _ -> assert false (* internally used in grammar only *) with Not_found -> if Option.is_empty lev then - error "A left-recursive notation must have an explicit level." + user_err Pp.(str "A left-recursive notation must have an explicit level.") else [],Option.get lev) | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) else [],Option.get lev | Some _ -> - if Option.is_empty lev then error "Cannot determine the level."; + if Option.is_empty lev then user_err Pp.(str "Cannot determine the level."); [],Option.get lev let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () with Not_found -> - error "Notations involving patterns of the form \"{ _ }\" are treated \n\ -specially and require that the notation \"{ _ }\" is already reserved." + user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\ +specially and require that the notation \"{ _ }\" is already reserved.") (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) let remove_curly_brackets l = @@ -1081,7 +1081,7 @@ let compute_syntax_data df modifiers = let mods = interp_modifiers modifiers in let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in - if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'."; + if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); let assoc = Option.append mods.assoc (Some NonA) in let toks = split_notation_string df in let recvars,mainvars,symbols = analyze_notation_tokens toks in @@ -1385,7 +1385,7 @@ let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> - error "Parsing rule for this notation has to be previously declared."); + user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) diff --git a/vernac/record.ml b/vernac/record.ml index 10207d0e0..5accc8e37 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -561,7 +561,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id in let isnot_class = match kind with Class false -> false | _ -> true in if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then - error "Priorities only allowed for type class substructures"; + user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) let (pl, ctx), arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a08c79c40..6c1d64cfe 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -139,7 +139,7 @@ let make_cases s = let show_match id = let patterns = try make_cases_aux (Nametab.global id) - with Not_found -> error "Unknown inductive type." + with Not_found -> user_err Pp.(str "Unknown inductive type.") in let pr_branch l = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" @@ -305,7 +305,7 @@ let print_strategy r = let key = match r with | VarRef id -> VarKey id | ConstRef cst -> ConstKey cst - | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable" + | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable") in let lvl = get_strategy oracle key in Feedback.msg_notice (pr_strategy (r, lvl)) @@ -451,8 +451,8 @@ let start_proof_and_print k l hook = concl (Tacticals.New.tclCOMPLETE tac) in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> - error "The statement obligations could not be resolved \ - automatically, write a statement definition first." + user_err Pp.(str "The statement obligations could not be resolved \ + automatically, write a statement definition first.") in Some hook else None in @@ -551,9 +551,9 @@ let vernac_inductive poly lo finite indl = indl; match indl with | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] -> - CErrors.error "The Record keyword is for types defined using the syntax { ... }." + user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.") | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> - CErrors.error "The Variant keyword does not support syntax { ... }." + user_err Pp.(str "The Variant keyword does not support syntax { ... }.") | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record (match b with Class _ -> Class false | _ -> b) poly finite id bl c oc fs @@ -564,16 +564,16 @@ let vernac_inductive poly lo finite indl = (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) poly finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> - CErrors.error "Inductive classes not supported" + user_err Pp.(str "Inductive classes not supported") | [ ( id , bl , c , Class _, _), _ :: _ ] -> - CErrors.error "where clause not supported for classes" + user_err Pp.(str "where clause not supported for classes") | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> - CErrors.error "where clause not supported for (co)inductive records" + user_err Pp.(str "where clause not supported for (co)inductive records") | _ -> let unpack = function | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn | ( (true,_),_,_,_,Constructors _),_ -> - CErrors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead." - | _ -> CErrors.error "Cannot handle mutually (co)inductive records." + user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.") + | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in do_mutual_inductive indl poly lo finite @@ -631,11 +631,11 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then - error "Modules and Module Types are not allowed inside sections."; + user_err Pp.(str "Modules and Module Types are not allowed inside sections."); let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument." + user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast @@ -649,7 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then - error "Modules and Module Types are not allowed inside sections."; + user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mexpr_ast_l with | [] -> check_no_pending_proofs (); @@ -674,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." + user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast @@ -694,7 +694,7 @@ let vernac_end_module export (loc,id as lid) = let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then - error "Modules and Module Types are not allowed inside sections."; + user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mty_ast_l with | [] -> @@ -722,7 +722,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." + user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_module_ast @@ -846,7 +846,7 @@ let vernac_set_end_tac tac = let env = Genintern.empty_glob_sign (Global.env ()) in let _, tac = Genintern.generic_intern env tac in if not (refining ()) then - error "Unknown command of the non proof-editing mode."; + user_err Pp.(str "Unknown command of the non proof-editing mode."); set_end_tac tac (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) @@ -903,7 +903,7 @@ let vernac_chdir = function (* Cd is typically used to control the output directory of extraction. A failed Cd could lead to overwriting .ml files so we make it an error. *) - CErrors.error ("Cd failed: " ^ err) + user_err Pp.(str ("Cd failed: " ^ err)) end; if_verbose Feedback.msg_info (str (Sys.getcwd())) @@ -972,7 +972,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let never_unfold_flag = List.mem `ReductionNeverUnfold flags in let err_incompat x y = - error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in + user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in if assert_flag && rename_flag then err_incompat "assert" "rename"; @@ -1018,7 +1018,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags | { name = Anonymous; notation_scope = Some _ } :: args -> check_extra_args args | _ -> - error "Extra notation scopes can be set on anonymous and explicit arguments only." + user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.") in let args, scopes = @@ -1032,12 +1032,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags in if Option.cata (fun n -> n > num_args) false nargs_for_red then - error "The \"/\" modifier should be put before any extra scope."; + user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); let scopes_specified = List.exists Option.has_some scopes in if scopes_specified && clear_scopes_flag then - error "The \"clear scopes\" flag is incompatible with scope annotations."; + user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); let names = List.map (fun { name } -> name) args in let names = names :: List.map (List.map fst) more_implicits in @@ -1062,7 +1062,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags | name1 :: names1, name2 :: names2 -> if Name.equal name1 name2 then name1 :: names_union names1 names2 - else error "Argument lists should agree on the names they provide." + else user_err Pp.(str "Argument lists should agree on the names they provide.") in let names = List.fold_left names_union [] names in @@ -1143,10 +1143,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let implicits_specified = match implicits with [[]] -> false | _ -> true in if implicits_specified && clear_implicits_flag then - error "The \"clear implicits\" flag is incompatible with implicit annotations"; + user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); if implicits_specified && default_implicits_flag then - error "The \"default implicits\" flag is incompatible with implicit annotations"; + user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) @@ -1452,8 +1452,8 @@ let vernac_set_strategy locality l = match smart_global r with | ConstRef sp -> EvalConstRef sp | VarRef id -> EvalVarRef id - | _ -> error - "cannot set an inductive type or a constructor as transparent" in + | _ -> user_err Pp.(str + "cannot set an inductive type or a constructor as transparent") in let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in Redexpr.set_strategy local l @@ -1463,8 +1463,8 @@ let vernac_set_opacity locality (v,l) = match smart_global r with | ConstRef sp -> EvalConstRef sp | VarRef id -> EvalVarRef id - | _ -> error - "cannot set an inductive type or a constructor as transparent" in + | _ -> user_err Pp.(str + "cannot set an inductive type or a constructor as transparent") in let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] @@ -1764,10 +1764,10 @@ let vernac_locate = let open Feedback in function let vernac_register id r = if Pfedit.refining () then - error "Cannot register a primitive while in proof editing mode."; + user_err Pp.(str "Cannot register a primitive while in proof editing mode."); let t = (Constrintern.global_reference (snd id)) in if not (isConst t) then - error "Register inline: a constant is expected"; + user_err Pp.(str "Register inline: a constant is expected"); let kn = destConst t in match r with | RegisterInline -> Global.register_inline (Univ.out_punivs kn) @@ -1780,7 +1780,7 @@ let vernac_focus gln = match gln with | None -> Proof.focus focus_command_cond () 1 p | Some 0 -> - CErrors.error "Invalid goal number: 0. Goal numbering starts with 1." + user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.") | Some n -> Proof.focus focus_command_cond () n p) @@ -1795,7 +1795,7 @@ let vernac_unfocused () = if Proof.unfocused p then Feedback.msg_notice (str"The proof is indeed fully unfocused.") else - error "The proof is not fully unfocused." + user_err Pp.(str "The proof is not fully unfocused.") (* BeginSubproof / EndSubproof. @@ -2081,7 +2081,7 @@ let check_vernac_supports_locality c l = | VernacDeclareReduction _ | VernacExtend _ | VernacInductive _) -> () - | Some _, _ -> CErrors.error "This command does not support Locality" + | Some _, _ -> user_err Pp.(str "This command does not support Locality") (* Vernaculars that take a polymorphism flag *) let check_vernac_supports_polymorphism c p = @@ -2095,7 +2095,7 @@ let check_vernac_supports_polymorphism c p = | VernacInstance _ | VernacDeclareInstances _ | VernacHints _ | VernacContext _ | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> () - | Some _, _ -> CErrors.error "This command does not support Polymorphism" + | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism") let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () @@ -2172,13 +2172,13 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacStm _ -> assert false (* Done by Stm *) | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c - | VernacProgram _ -> CErrors.error "Program mode specified twice" + | VernacProgram _ -> user_err Pp.(str "Program mode specified twice") | VernacLocal (b, c) when Option.is_empty locality -> aux ~locality:b ?polymorphism isprogcmd c | VernacPolymorphic (b, c) when polymorphism = None -> aux ?locality ~polymorphism:b isprogcmd c - | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice" - | VernacLocal _ -> CErrors.error "Locality specified twice" + | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice") + | VernacLocal _ -> user_err Pp.(str "Locality specified twice") | VernacFail v -> with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> |