diff options
| author | Emilio Jesus Gallego Arias | 2017-03-15 20:48:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-05-27 22:35:10 +0200 |
| commit | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (patch) | |
| tree | 78c30edd51e65c8e7014ac360c5027da77ff20b2 | |
| parent | 2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff) | |
[cleanup] Unify all calls to the error function.
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
116 files changed, 437 insertions, 421 deletions
diff --git a/checker/check.ml b/checker/check.ml index 11678fa6bb..6d93c11eac 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 5cadfe7b94..e00f47a540 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 7b59c6b986..bce40861cf 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 27f79e7963..0482912b0a 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 8f23a38afc..9e417a8eb5 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 07dda8a06d..bed31143bf 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 28c0126b41..82f09cf4b0 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 53d80c6d55..c70cd5c8ce 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 a290b240d8..2d04b77e46 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 24e6008d34..8cac783753 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 d52c184623..0b0c0f5bfb 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -162,7 +162,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 e5ac3792d6..c0485e4e76 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 8ade6cb996..b677705bc9 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 7f80d40d64..ddfc0e39dd 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 dc68220575..acef901432 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 c7078cf2a0..4dcf287efc 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 74644b206a..6f91009111 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 1fe63c19c4..a79f10df6b 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 3f1cf92487..4533169804 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 d8d365c347..4f4b641b44 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 f5b3f4e007..afdbe0c0dc 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 6bd82170e6..26d0617683 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 d0593c0e05..502a10113d 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 caaaff1b89..f5e8e86530 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 d0fdf9fdae..f779f68be4 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 03562d9f31..a4296a530c 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 b55fd80c68..b0e77a4c90 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 0665a8ce73..ca0838575e 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 2755946abc..d004fd6711 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 3a263b1e12..08c33b5c15 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 9b4fc99857..a803771cbc 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 a63264b669..885185da1a 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 ddd2ed6afa..4ad4e261d7 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 dd74e192ff..50f28b0205 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 2b3381fa7c..5a5f99cc51 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 1027e291ce..2e4e98013e 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 b5d0780bd5..893605499c 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 12d7f06603..b3ab29cced 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 322fbcea74..2c85b185c4 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 0692c88cd1..b580fb5925 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 d8e3821557..4399fc561f 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 8d0cc4a0db..3c81564e34 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 5a1e7c26a1..4c6355f61c 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 2d18b66054..826afc35b6 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 25d8f8c832..f397f84a8b 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -513,11 +513,11 @@ let rec fourier () = with NoIneq -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.error "No inequalities"; + if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] - then CErrors.error "fourier failed" + then CErrors.user_err Pp.(str "fourier failed") (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 55d361e3d2..64f7813a32 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -820,10 +820,10 @@ let build_proof build_proof new_finalize {dyn_infos with info = f } g end | Fix _ | CoFix _ -> - error ( "Anonymous local (co)fixpoints are not handled yet") + user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) - | Proj _ -> error "Prod" - | Prod _ -> error "Prod" + | Proj _ -> user_err Pp.(str "Prod") + | Prod _ -> user_err Pp.(str "Prod") | LetIn _ -> let new_infos = { dyn_infos with @@ -1097,7 +1097,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Global.env ()) (Evd.empty) (EConstr.of_constr body) - | None -> error ( "Cannot define a principle over an axiom ") + | None -> user_err Pp.(str "Cannot define a principle over an axiom ") in let fbody = get_body fnames.(fun_num) in let f_ctxt,f_body = decompose_lam (project g) fbody in @@ -1199,7 +1199,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam bs.(num), List.rev_map var_of_decl princ_params)) ),num - | _ -> error "Not a mutual block" + | _ -> user_err Pp.(str "Not a mutual block") in let info = {infos with @@ -1594,7 +1594,7 @@ let prove_principle_for_gen let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with - | Undefined -> error "No tcc proof !!" + | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 529b91c4ca..18d63dd94b 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 5e6128b1b9..1db8be0818 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 7f2b21e79d..d8614f376d 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 5abcb100f7..0361e8cb13 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 ab83cb15a6..74c0eb4cc7 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 ea985ddecd..91dac303a7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -502,13 +502,13 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match EConstr.kind sigma c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> CErrors.error "decompose_lam_n: not enough abstractions" + | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8c972cd7cf..8747efc02b 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 b99a05dfbc..b2c8489ce1 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 c463093553..e206955acb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -136,7 +136,7 @@ let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" - with Not_found -> error "module Recdef not loaded" + with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter = function () -> (constr_of_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") @@ -323,8 +323,8 @@ let check_not_nested sigma forbidden e = | Construct _ -> () | Case(_,t,e,a) -> check_not_nested t;check_not_nested e;Array.iter check_not_nested a - | Fix _ -> error "check_not_nested : Fix" - | CoFix _ -> error "check_not_nested : Fix" + | Fix _ -> user_err Pp.(str "check_not_nested : Fix") + | CoFix _ -> user_err Pp.(str "check_not_nested : Fix") in try check_not_nested e @@ -430,8 +430,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = let sigma = project g in match EConstr.kind sigma expr_info.info with - | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint" - | Proj _ -> error "Function cannot treat projections" + | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") + | Proj _ -> user_err Pp.(str "Function cannot treat projections") | LetIn(na,b,t,e) -> begin let new_continuation_tac = @@ -1304,7 +1304,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in let na = next_global_ident_away name [] in if Termops.occur_existential sigma gls_type then - CErrors.error "\"abstract\" cannot handle existentials"; + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.tag na) in diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 470a93f2bc..bf84f61a5b 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 a3310c2d8c..fdb8d34618 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 cbd8a7f0fe..ed80dd7ae3 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1084,7 +1084,7 @@ let decompose l c = let sigma = Tacmach.New.project gl in let to_ind c = if isInd sigma c then fst (destInd sigma c) - else error "not an inductive type" + else user_err Pp.(str "not an inductive type") in let l = List.map to_ind l in Elim.h_decompose l c diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 257100b012..1404b1c1f1 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 75ab1c5ee6..a001c6a2ba 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 e8c9f4ebaa..51729f4c6e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -241,7 +241,7 @@ end) = struct let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs - else error "build_signature: no constraint can apply on a dependent argument" + else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") | _, [] -> (match finalcstr with @@ -478,7 +478,7 @@ type hypinfo = { let get_symmetric_proof b = if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof -let error_no_relation () = error "Cannot find a relation to rewrite." +let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.") let rec decompose_app_rel env evd t = (** Head normalize for compatibility with the old meta mechanism *) @@ -531,7 +531,7 @@ let decompose_applied_relation env sigma (c,l) = let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c - | None -> error "Cannot find an homogeneous relation to rewrite." + | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.") let rewrite_db = "rewrite" @@ -837,7 +837,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then - error "Cannot rewrite inside dependent arguments of a function"; + user_err Pp.(str "Cannot rewrite inside dependent arguments of a function"); x :: acc, x :: subst, evars, sigargs, x :: typeargs') ([], [], evars, sigargs, []) args args' in @@ -1425,7 +1425,7 @@ module Strategies = let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> - error "fold: the term is not unfoldable !" + user_err Pp.(str "fold: the term is not unfoldable !") in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in @@ -2204,7 +2204,7 @@ let setoid_symmetry_in id = let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "Cannot find an equivalence relation to rewrite." + | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.") in let others,(c1,c2) = split_last_two args in let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4d7b0f9296..75f89a81e1 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 6c7eb8c899..e431a13bc2 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 632b9dac14..af8107025a 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -462,7 +462,7 @@ let theoremedeszeros_termes lp = lexico:=true; |7 -> sinfo "ordre lexico computation with sugar, division by pairs"; lexico:=true; - | _ -> error "nsatz: bad parameter" + | _ -> user_err Pp.(str "nsatz: bad parameter") ); let lvar = List.init nvars (fun i -> Printf.sprintf "x%i" (i + 1)) in let lvar = ["a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z"] @ lvar in @@ -549,5 +549,5 @@ let nsatz_compute t = let lpol = try nsatz t with Ideal.NotInIdeal -> - error "nsatz cannot solve this problem" in + user_err Pp.(str "nsatz cannot solve this problem") in return_term lpol diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 334baec8d5..d3ca874bdd 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 6b711a1761..ce7ffb1e7e 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 c649cfb2c6..db69f1b404 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -183,7 +183,7 @@ type inversion_scheme = { goal [gl]. This function uses the auxiliary functions [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) -let i_can't_do_that () = error "Quote: not a simple fixpoint" +let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint") let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c) diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index c2d7d50502..6479c683b2 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 e566050766..fdcd622994 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 e20e78b1a7..0e1225ada8 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 862e44ccad..6b752fb4b0 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 edcfa99c86..2cb837ba03 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 42aaf3a227..b944da7500 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1051,7 +1051,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 @@ -1070,7 +1070,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 @@ -1108,10 +1108,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 @@ -1245,7 +1245,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 4ada91eb59..98e71c7fd9 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 429e5005ec..7f3bafc685 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 e4fbf8d542..211ffbe01e 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 0228f63cdc..afaa20b6f6 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 a8012d35f8..1c8ad0cddd 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 7d65925e57..8e190f40b9 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 117ed338ee..e7c9635829 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 67221046bd..3d41d2ddd5 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 919e95a8ee..d7b4842810 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 cac6c50572..d1643a8c7d 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 74998349be..b08666483e 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 d1ba1a4a10..99d07601c4 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 70de65acdc..0f7da36133 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 d4f7afb38c..ebe68680fb 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 9e0a2a03eb..33a86402ef 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 b9c9257969..b1fe128a24 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 54345abd97..cd2cfbd32f 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 92b4e788a2..aaceb7b762 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 b2103489a7..2aa620c1da 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 95aee72cb5..4d2f534a76 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 b2ea3341b4..9f50ab589d 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 918371d55e..46d66b9d06 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 e87368dec6..986f531397 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 d023b45682..bcd31cb7e7 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 70d6fe90c5..839ec4ce12 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 @@ -1887,7 +1887,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 e6edae7ef6..48a7b3f75c 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 dce98eed74..fd5eabe648 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 5c4b73a622..b951e7ceba 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 fe9cb123ce..c495b5ece2 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 c713a31fa3..c7847e412b 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 930b092d3b..044399544a 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 7fa8fd58db..defc803381 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 ac1e623d76..7834b5113b 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 7e81aa20ad..a61ade7849 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 5843da31ed..004083dcf9 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 8a9bbb8846..4b29700e53 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 @@ -1122,7 +1122,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 @@ -1262,8 +1262,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 @@ -1282,7 +1282,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 c6588684a4..f3259f1f3b 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 b21e80bef1..a782213015 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 @@ -497,7 +497,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 c67a3302ff..d6ae0ea86f 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 03640676e6..a25acb0d34 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 fb7c729412..42494dd28a 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 10207d0e04..5accc8e379 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 a08c79c400..6c1d64cfe9 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) -> |