diff options
74 files changed, 522 insertions, 484 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c922503aa..304ac5d78 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -98,7 +98,7 @@ let ids_of_ctxt ctxt = (function c -> match kind_of_term c with | Var id -> id | _ -> - error "arbitrary substitution of references not implemented") + error "Arbitrary substitution of references not implemented.") ctxt) let idopt_of_name = function @@ -973,7 +973,7 @@ and raw_of_eqn env constr construct_nargs branch = buildrec new_ids (pat::patlist) new_env (n-1) b | _ -> - error "Unsupported branch in case-analysis while printing pattern" + error "Unsupported branch in case-analysis while printing pattern." in buildrec [] [] env construct_nargs branch diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6fc65e9fb..d802770f0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -99,7 +99,8 @@ let explain_bad_explicitation_number n po = str "Bad explicitation name: found " ++ pr_id id ++ str" but was expecting " ++ s -let explain_internalisation_error = function +let explain_internalisation_error e = + let pp = match e with | VariableCapture id -> explain_variable_capture id | WrongExplicitImplicit -> explain_wrong_explicit_implicit | IllegalMetavariable -> explain_illegal_metavariable @@ -107,16 +108,17 @@ let explain_internalisation_error = function | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 - | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po + | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in + pp ++ str "." let error_unbound_patvar loc n = user_err_loc (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ - str " is unbound") + str " is unbound.") let error_bad_inductive_type loc = user_err_loc (loc,"",str - "This should be an inductive type applied to names or \"_\"") + "This should be an inductive type applied to names or \"_\".") let error_inductive_parameter_not_implicit loc = user_err_loc (loc,"", str @@ -180,7 +182,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes = make_current_scope (Option.get !idscopes) <> make_current_scope (scopt,scopes) then user_err_loc (loc,"set_var_scope", - pr_id id ++ str " already occurs in a different scope") + pr_id id ++ str " already occurs in a different scope.") else idscopes := Some (scopt,scopes) @@ -300,7 +302,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id = try match List.assoc id unbndltacvars with | None -> user_err_loc (loc,"intern_var", - str "variable " ++ pr_id id ++ str " should be bound to a term") + str "variable " ++ pr_id id ++ str " should be bound to a term.") | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> (* Is [id] a goal or section variable *) @@ -319,14 +321,14 @@ let find_appl_head_data (_,_,_,(_,impls)) = function | x -> x,[],[],[] let error_not_enough_arguments loc = - user_err_loc (loc,"",str "Abbreviation is not applied enough") + user_err_loc (loc,"",str "Abbreviation is not applied enough.") let check_no_explicitation l = let l = List.filter (fun (a,b) -> b <> None) l in if l <> [] then let loc = fst (Option.get (snd (List.hd l))) in user_err_loc - (loc,"",str"Unexpected explicitation of the argument of an abbreviation") + (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env args = @@ -436,7 +438,7 @@ let check_number_of_pattern loc n l = let check_or_pat_variables loc ids idsl = if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then user_err_loc (loc, "", str - "The components of this disjunctive pattern must bind the same variables") + "The components of this disjunctive pattern must bind the same variables.") let check_constructor_length env loc cstr pl pl0 = let n = List.length pl + List.length pl0 in @@ -463,7 +465,7 @@ let message_redundant_alias (id1,id2) = (* Expanding notations *) let error_invalid_pattern_notation loc = - user_err_loc (loc,"",str "Invalid notation for pattern") + user_err_loc (loc,"",str "Invalid notation for pattern.") let chop_aconstr_constructor loc (ind,k) args = let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in @@ -671,9 +673,9 @@ let locate_if_isevar loc na = function let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = if List.mem id indnames then - errorlabstrm "" (str "A parameter or name of an inductive type " ++ - pr_id id ++ str " must not be used as a bound variable in the type \ -of its constructor") + errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++ + pr_id id ++ strbrk " must not be used as a bound variable in the type \ +of its constructor.") let push_name_env lvar (ids,tmpsc,scopes as env) = function | Anonymous -> env @@ -734,11 +736,11 @@ let check_projection isproj nargs r = (try let n = Recordops.find_projection_nparams ref + 1 in if nargs <> n then - user_err_loc (loc,"",str "Projection has not the right number of explicit parameters"); + user_err_loc (loc,"",str "Projection has not the right number of explicit parameters."); with Not_found -> user_err_loc - (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection")) - | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection") + (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection.")) + | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.") | _, None -> () let get_implicit_name n imps = @@ -763,10 +765,11 @@ let extract_explicit_arg imps args = let id = match pos with | ExplByName id -> if not (exists_implicit_name id imps) then - user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id); + user_err_loc + (loc,"",str "Wrong argument name: " ++ pr_id id ++ str "."); if List.mem_assoc id eargs then user_err_loc (loc,"",str "Argument name " ++ pr_id id - ++ str " occurs more than once"); + ++ str " occurs more than once."); id | ExplByPos (p,_id) -> let id = @@ -775,11 +778,12 @@ let extract_explicit_arg imps args = if not (is_status_implicit imp) then failwith "imp"; name_of_implicit imp with Failure _ (* "nth" | "imp" *) -> - user_err_loc (loc,"",str"Wrong argument position: " ++ int p) + user_err_loc + (loc,"",str"Wrong argument position: " ++ int p ++ str ".") in if List.mem_assoc id eargs then user_err_loc (loc,"",str"Argument at position " ++ int p ++ - str " is mentioned more than once"); + str " is mentioned more than once."); id in ((id,(loc,a))::eargs,rargs) in aux args @@ -1003,7 +1007,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let nal = List.map (function | RHole loc -> Anonymous | RVar (_,id) -> Name id - | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in + | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in let parnal,realnal = list_chop nparams nal in if List.exists ((<>) Anonymous) parnal then error_inductive_parameter_not_implicit loc; @@ -1075,7 +1079,8 @@ let internalise sigma globalenv env allow_patvar lvar c = if eargs <> [] then (let (id,(loc,_)) = List.hd eargs in user_err_loc (loc,"",str "Not enough non implicit - arguments to accept the argument bound to " ++ pr_id id)); + arguments to accept the argument bound to " ++ + pr_id id ++ str".")); [] | ([], rargs) -> assert (eargs = []); diff --git a/interp/coqlib.ml b/interp/coqlib.ml index ecc48dfe2..845707f9e 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -70,7 +70,7 @@ let check_required_library d = (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(string_of_dirpath dir)^" has to be required first") + error ("Library "^(string_of_dirpath dir)^" has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/interp/notation.ml b/interp/notation.ml index bafce17af..164423ead 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -78,7 +78,7 @@ let declare_scope scope = let find_scope scope = try Gmap.find scope !scope_map - with Not_found -> error ("Scope "^scope^" is not declared") + with Not_found -> error ("Scope "^scope^" is not declared.") let check_scope sc = let _ = find_scope sc in () @@ -159,7 +159,7 @@ let find_delimiters_scope loc key = try Gmap.find key !delimiters_map with Not_found -> user_err_loc - (loc, "find_delimiters", str ("Unknown scope delimiting key "^key)) + (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^".")) (* Uninterpretation tables *) @@ -251,7 +251,7 @@ let check_required_module loc sc (sp,d) = with Not_found -> user_err_loc (loc,"prim_token_interpreter", str ("Cannot interpret in "^sc^" without requiring first module " - ^(list_last d))) + ^(list_last d)^".")) (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -348,7 +348,7 @@ let interp_prim_token_gen g loc p local_scopes = user_err_loc (loc,"interp_prim_token", (match p with | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n - | String s -> str "No interpretation for string " ++ qs s)) + | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token = interp_prim_token_gen (fun x -> x) @@ -361,7 +361,7 @@ let rec interp_notation loc ntn local_scopes = try find_interpretation (find_notation ntn) scopes with Not_found -> user_err_loc - (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"")) + (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) let uninterp_notations c = Gmapl.find (rawconstr_key c) !notations_key_table @@ -625,12 +625,12 @@ let global_reference_of_notation test (ntn,(sc,c,_)) = | _ -> None let error_ambiguous_notation loc _ntn = - user_err_loc (loc,"",str "Ambiguous notation") + user_err_loc (loc,"",str "Ambiguous notation.") let error_notation_not_reference loc ntn = user_err_loc (loc,"", str "Unable to interpret " ++ quote (str ntn) ++ - str " as a reference") + str " as a reference.") let interp_notation_as_global_reference loc test ntn = let ntns = browse_notation true ntn !scope_map in diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 8ded0a35b..c684c6adb 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -150,7 +150,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) - -> error "Unsupported construction in recursive notations" + -> error "Unsupported construction in recursive notations." | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _ -> false @@ -168,13 +168,13 @@ let discriminate_patterns foundvars nl l1 l2 = | _ -> compare_rawconstr (aux (n+1)) c1 c2 in let l = list_map2_i aux 0 l1 l2 in if not (List.for_all ((=) true) l) then - error "Both ends of the recursive pattern differ"; + error "Both ends of the recursive pattern differ."; match !diff with - | None -> error "Both ends of the recursive pattern are the same" + | None -> error "Both ends of the recursive pattern are the same." | Some (x,y,_ as discr) -> List.iter (fun id -> if List.mem id !foundvars - then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part"; + then errorlabstrm "" (strbrk "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part."); foundvars := id::!foundvars) [x;y]; discr @@ -212,7 +212,7 @@ let aconstr_and_vars_of_rawconstr a = Array.iter (fun id -> found := 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"; + error "Binders marked as implicit not allowed in notations."; add_name found na; (na,Option.map aux oc,aux b))) dll in ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | RCast (_,c,k) -> ACast (aux c, @@ -223,17 +223,17 @@ let aconstr_and_vars_of_rawconstr a = | RRef (_,r) -> ARef r | RPatVar (_,(_,n)) -> APatVar n | RDynamic _ | REvar _ -> - error "Existential variables not allowed in notations" + error "Existential variables not allowed in notations." (* Recognizing recursive notations *) and terminator_of_pat f1 ll1 lr1 = function | RApp (loc,f2,l2) -> - if not (eq_rawconstr f1 f2) then error - "Cannot recognize the same head to both ends of the recursive pattern"; + if not (eq_rawconstr f1 f2) then errorlabstrm "" + (strbrk "Cannot recognize the same head to both ends of the recursive pattern."); let nl = List.length ll1 in let nr = List.length lr1 in if List.length l2 <> nl + nr + 1 then - error "Both ends of the recursive pattern have different lengths"; + error "Both ends of the recursive pattern have different lengths."; let ll2,l2' = list_chop nl l2 in let t = List.hd l2' and lr2 = List.tl l2' in let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in @@ -241,8 +241,8 @@ let aconstr_and_vars_of_rawconstr a = if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2) else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in (if order then y else x),(if order then x else y), aux iter, aux t, order - | _ -> error "One end of the recursive pattern is not an application" - + | _ -> error "One end of the recursive pattern is not an application." + and make_aconstr_list f args = let rec find_patterns acc = function | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var -> @@ -250,7 +250,7 @@ let aconstr_and_vars_of_rawconstr a = let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in AList (x,y,iter,term,lassoc) | a::l -> find_patterns (a::acc) l - | [] -> error "Ill-formed recursive notation" + | [] -> error "Ill-formed recursive notation." in find_patterns [] args in @@ -262,7 +262,7 @@ let aconstr_of_rawconstr vars a = let a,foundvars = aconstr_and_vars_of_rawconstr a in let check_type x = if not (List.mem x foundvars) then - error ((string_of_id x)^" is unbound in the right-hand-side") in + error ((string_of_id x)^" is unbound in the right-hand-side.") in List.iter check_type vars; a @@ -853,7 +853,7 @@ let coerce_to_id = function | CRef (Ident (loc,id)) -> (loc,id) | a -> user_err_loc (constr_loc a,"coerce_to_id", - str "This expression should be a simple identifier") + str "This expression should be a simple identifier.") (* Used in correctness and interface *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e9f8f89ad..f70690af6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -263,7 +263,7 @@ let typecheck_inductive env mie = | Prop Pos when engagement env <> Some ImpredicativeSet -> (* Predicative set: check that the content is indeed predicative *) if not (is_type0m_univ lev) & not (is_type0_univ lev) then - error "Large non-propositional inductive types must be in Type"; + error "Large non-propositional inductive types must be in Type."; Inl (info,full_arity,s), cst | Prop _ -> Inl (info,full_arity,s), cst in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3b64a2c09..8ff8ddb85 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -218,7 +218,7 @@ let type_of_constructor cstr (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 error "Not enough constructors in the type."; constructor_instantiate (fst ind) mib specif.(i-1) let arities_of_specif kn (mib,mip) = diff --git a/kernel/modops.ml b/kernel/modops.ml index 26030b9e9..d903d4b32 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -22,51 +22,51 @@ open Mod_subst let error_existing_label l = - error ("The label "^string_of_label l^" is already declared") + error ("The label "^string_of_label l^" is already declared.") -let error_declaration_not_path _ = error "Declaration is not a path" +let error_declaration_not_path _ = error "Declaration is not a path." -let error_application_to_not_path _ = error "Application to not path" +let error_application_to_not_path _ = error "Application to not path." -let error_not_a_functor _ = error "Application of not a functor" +let error_not_a_functor _ = error "Application of not a functor." -let error_incompatible_modtypes _ _ = error "Incompatible module types" +let error_incompatible_modtypes _ _ = error "Incompatible module types." -let error_not_equal _ _ = error "Not equal modules" +let error_not_equal _ _ = error "Non equal modules." -let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match") +let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.") -let error_no_such_label l = error ("No such label "^string_of_label l) +let error_no_such_label l = error ("No such label "^string_of_label l^".") let error_incompatible_labels l l' = error ("Opening and closing labels are not the same: " ^string_of_label l^" <> "^string_of_label l'^" !") let error_result_must_be_signature () = - error "The result module type must be a signature" + error "The result module type must be a signature." let error_signature_expected mtb = - error "Signature expected" + error "Signature expected." let error_no_module_to_end _ = - error "No open module to end" + error "No open module to end." let error_no_modtype_to_end _ = - error "No open module type to end" + error "No open module type to end." let error_not_a_modtype_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module type")) + user_err_loc (loc,"",str ("\""^s^"\" is not a module type.")) let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module")) + user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) let error_not_a_module s = error_not_a_module_loc dummy_loc s let error_not_a_constant l = - error ("\""^(string_of_label l)^"\" is not a constant") + error ("\""^(string_of_label l)^"\" is not a constant.") let error_with_incorrect l = - error ("Incorrect constraint for label \""^(string_of_label l)^"\"") + error ("Incorrect constraint for label \""^(string_of_label l)^"\".") let error_a_generative_module_expected l = error ("The module " ^ string_of_label l ^ " is not generative. Only " ^ @@ -79,7 +79,7 @@ let error_local_context lo = error ("The local context is not empty.") | (Some l) -> error ("The local context of the component "^ - (string_of_label l)^" is not empty") + (string_of_label l)^" is not empty.") let error_no_such_label_sub l l1 l2 = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fbd4901d6..eef2d675c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -163,7 +163,7 @@ let safe_push_named (id,_,_ as d) env = let _ = try let _ = lookup_named id env in - error ("identifier "^string_of_id id^" already defined") + error ("Identifier "^string_of_id id^" already defined.") with Not_found -> () in Environ.push_named d env @@ -446,7 +446,7 @@ let end_module l restype senv = let senv = add_constraints (struct_expr_constraints struct_expr) senv in let msid,str = match (eval_struct senv.env struct_expr) with | SEBstruct(msid,str_l) -> msid,str_l - | _ -> error ("You cannot Include a higher-order Module or Module Type" ) + | _ -> error ("You cannot Include a higher-order Module or Module Type.") in let mp_sup = senv.modinfo.modpath in let str1 = subst_signature_msid msid mp_sup str in @@ -660,7 +660,7 @@ let check_engagement env c = | Some ImpredicativeSet, Some ImpredicativeSet -> () | _, None -> () | _, Some ImpredicativeSet -> - error "Needs option -impredicative-set" + error "Needs option -impredicative-set." let set_engagement c senv = {senv with @@ -739,9 +739,10 @@ let check_imports senv needed = try let actual_stamp = List.assoc id imports in if stamp <> actual_stamp then - error ("Inconsistent assumptions over module " ^(string_of_dirpath id)) + error + ("Inconsistent assumptions over module "^(string_of_dirpath id)^".") with Not_found -> - error ("Reference to unknown module " ^ (string_of_dirpath id)) + error ("Reference to unknown module "^(string_of_dirpath id)^".") in List.iter check needed diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2b28a7147..ccc62b756 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -60,7 +60,7 @@ let safe_push_named (id,_,_ as d) env = let _ = try let _ = lookup_named id env in - error ("identifier "^string_of_id id^" already defined") + error ("Identifier "^string_of_id id^" already defined.") with Not_found -> () in push_named d env diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index f51cc0869..bd688bcdd 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -234,7 +234,7 @@ let rec interp_entry_name up_level s = try get_entry (get_univ "prim") s with _ -> try get_entry (get_univ "constr") s - with _ -> error ("Unknown entry "^s) + with _ -> error ("Unknown entry "^s^".") in let o = object_of_typed_entry e in let t = type_of_typed_entry e in @@ -254,7 +254,7 @@ let get_tactic_entry n = else if 1<=n && n<5 then weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n)) else - error ("Invalid Tactic Notation level: "^(string_of_int n)) + error ("Invalid Tactic Notation level: "^(string_of_int n)^".") (* Declaration of the tactic grammar rule *) @@ -267,7 +267,7 @@ let add_tactic_entry (key,lev,prods,tac) = let rules = if lev = 0 then begin if not (head_is_ident prods) then - error "Notation for simple tactic must start with an identifier"; + error "Notation for simple tactic must start with an identifier."; let mkact s tac loc l = (TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in make_rule univ (mkact key tac) mkprod prods diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml index 8c570b0fd..f9ca94ff6 100644 --- a/parsing/g_ascii_syntax.ml +++ b/parsing/g_ascii_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) open Pp open Util @@ -53,7 +53,7 @@ let interp_ascii_string dloc s = then int_of_string s else user_err_loc (dloc,"interp_ascii_string", - str "Expects a single character or a three-digits ascii code") in + str "Expects a single character or a three-digits ascii code.") in interp_ascii dloc p let uninterp_ascii r = diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 476c0913f..b8dcf8e99 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -47,7 +47,7 @@ let rec index_and_rec_order_of_annot loc bl ann = | lids, (Some (loc, n), ro) -> if List.exists (fun (_, x) -> x = Name n) lids then Some (loc, n), ro - else user_err_loc(loc,"index_of_annot", Pp.str"no such fix variable") + else user_err_loc(loc,"index_of_annot", Pp.str"No such fix variable.") | _, (None, r) -> None, r let mk_fixb (id,bl,ann,body,(loc,tyc)) = @@ -61,7 +61,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofixb", - Pp.str"Annotation forbidden in cofix expression")) (fst ann) in + Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with Some ty -> ty | None -> CHole (loc, None) in @@ -326,7 +326,7 @@ GEXTEND Gram | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", - Pp.str "Constructor expected")) + Pp.str "Constructor expected.")) | p = pattern; "as"; id = ident -> CPatAlias (loc, p, id) ] | "1" LEFTA diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index f12ab6bee..7cef2fac0 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -122,7 +122,7 @@ let int31_of_pos_bigint dloc n = RApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers") + Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -212,7 +212,7 @@ let bigN_of_pos_bigint dloc n = result hght (word_of_pos_bigint dloc hght n) let bigN_error_negative dloc = - Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers") + Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index deedf957d..c24534e2d 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -31,7 +31,7 @@ let my_int_of_string loc s = if n > 1024 * 2048 then raise Exit; n with Failure _ | Exit -> - Util.user_err_loc (loc,"",Pp.str "cannot support a so large number.") + Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") GEXTEND Gram GLOBAL: @@ -89,7 +89,7 @@ GEXTEND Gram ; ne_string: [ [ s = STRING -> - if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s + if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s ] ] ; dirpath: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index bea3929df..a1fd1649e 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -131,15 +131,15 @@ 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 (snd x) ids - with Not_found -> error "no such fix variable") - | _ -> error "cannot guess decreasing argument of fix" in + with Not_found -> error "No such fix variable.") + | _ -> error "Cannot guess decreasing argument of fix." in (id,n,CProdN(loc,bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = let _ = Option.map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofix_tac", - Pp.str"Annotation forbidden in cofix expression")) ann in + Pp.str"Annotation forbidden in cofix expression.")) ann in (id,CProdN(loc,bl,ty)) (* Functions overloaded by quotifier *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 83b238953..5f656ed5c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -113,7 +113,7 @@ let test_plurial_form = function let no_coercion loc (c,x) = if c then Util.user_err_loc - (loc,"no_coercion",Pp.str"no coercion allowed here"); + (loc,"no_coercion",str"No coercion allowed here."); x (* Gallina declarations *) @@ -271,7 +271,7 @@ GEXTEND Gram Some (loc, id) else Util.user_err_loc (loc,"Fixpoint", - Pp.str "No argument named " ++ Nameops.pr_id id)) + str "No argument named " ++ Nameops.pr_id id ++ str".")) | None -> (* If there is only one argument, it is the recursive one, otherwise, we search the recursive index later *) @@ -311,7 +311,7 @@ GEXTEND Gram LocalRawAssum(l,ty) -> (l,ty) | LocalRawDef _ -> Util.user_err_loc - (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ] + (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] ; *) (* ... with coercions *) diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index a9f3fd487..e1e334be6 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -31,7 +31,7 @@ type xml = XmlTag of loc * string * attribute list * xml list let check_tags loc otag ctag = if otag <> ctag then user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ - str "does not match open xml tag " ++ str otag) + str "does not match open xml tag " ++ str otag ++ str ".") let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e) @@ -55,11 +55,19 @@ GEXTEND Gram ; END +(* Errors *) + +let error_expect_one_argument loc = + user_err_loc (loc,"",str "wrong number of arguments (expect one).") + +let error_expect_no_argument loc = + user_err_loc (loc,"",str "wrong number of arguments (expect none).") + (* Interpreting attributes *) let nmtoken (loc,a) = try int_of_string a - with Failure _ -> user_err_loc (loc,"",str "nmtoken expected") + with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") let interp_xml_attr_qualid = function | "uri", s -> qualid_of_string s @@ -94,7 +102,7 @@ let sort_of_cdata (loc,a) = match a with | "Prop" -> RProp Null | "Set" -> RProp Pos | "Type" -> RType None - | _ -> user_err_loc (loc,"",str "sort expected") + | _ -> user_err_loc (loc,"",str "sort expected.") let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) @@ -188,18 +196,18 @@ let rec interp_xml_constr = function RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2)) | XmlTag (loc,"SORT",al,[]) -> RSort (loc, get_xml_sort al) - | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) + | XmlTag (loc,s,_,_) -> + user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") and interp_xml_tag s = function | XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl) | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", - str "Expect tag " ++ str s ++ str " but find " ++ str s) + str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".") and interp_xml_constr_alias s x = match interp_xml_tag s x with | (_,_,[x]) -> interp_xml_constr x - | (loc,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + | (loc,_,_) -> error_expect_one_argument loc and interp_xml_term x = interp_xml_constr_alias "term" x and interp_xml_type x = interp_xml_constr_alias "type" x @@ -215,8 +223,7 @@ and interp_xml_substitution x = interp_xml_constr_alias "substitution" x and interp_xml_decl_alias s x = match interp_xml_tag s x with | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x) - | (loc,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + | (loc,_,_) -> error_expect_one_argument loc and interp_xml_def x = interp_xml_decl_alias "def" x and interp_xml_decl x = interp_xml_decl_alias "decl" x @@ -227,17 +234,17 @@ and interp_xml_recursionOrder x = match s with "Structural" -> (match l with [] -> RStructRec - | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)")) + | _ -> error_expect_no_argument loc) | "WellFounded" -> (match l with [c] -> RWfRec (interp_xml_type c) - | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) + | _ -> error_expect_one_argument loc) | "Measure" -> (match l with [c] -> RMeasureRec (interp_xml_type c) - | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) + | _ -> error_expect_one_argument loc) | _ -> - user_err_loc (locs,"",str "invalid recursion order") + user_err_loc (locs,"",str "Invalid recursion order.") and interp_xml_FixFunction x = match interp_xml_tag "FixFunction" x with @@ -248,15 +255,15 @@ and interp_xml_FixFunction x = | (loc,al,[x1;x2]) -> ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec), (get_xml_name al, interp_xml_type x1, interp_xml_body x2)) - | (loc,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + | (loc,_,_) -> + error_expect_one_argument loc and interp_xml_CoFixFunction x = match interp_xml_tag "CoFixFunction" x with | (loc,al,[x1;x2]) -> (get_xml_name al, interp_xml_type x1, interp_xml_body x2) | (loc,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + error_expect_one_argument loc (* Interpreting tactic argument *) @@ -266,7 +273,8 @@ let rec interp_xml_tactic_arg = function | XmlTag (loc,"CALL",al,xl) -> let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl) - | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) + | XmlTag (loc,s,_,_) -> + user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") let parse_tactic_arg ch = interp_xml_tactic_arg diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index 5d57c49db..bfbe54c28 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -57,7 +57,7 @@ let pos_of_bignat dloc x = let error_non_positive dloc = user_err_loc (dloc, "interp_positive", - str "Only strictly positive numbers in type \"positive\"") + str "Only strictly positive numbers in type \"positive\".") let interp_positive dloc n = if is_strictly_pos n then pos_of_bignat dloc n @@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n = RRef (dloc, glob_N0) let error_negative dloc = - user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\"") + user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") let n_of_int dloc n = if is_pos_or_zero n then n_of_binnat dloc true n diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index f9c2f90dd..cee08f234 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -247,7 +247,7 @@ let get_entry (u, utab) s = Hashtbl.find utab s with Not_found -> errorlabstrm "Pcoq.get_entry" - (str "unknown grammar entry " ++ str u ++ str ":" ++ str s) + (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".") let new_entry etyp (u, utab) s = let ename = u ^ ":" ^ s in @@ -307,12 +307,12 @@ let get_generic_entry s = try object_of_typed_entry (Hashtbl.find utab s) with Not_found -> - error ("unknown grammar entry "^u^":"^s) + error ("Unknown grammar entry "^u^":"^s^".") let get_generic_entry_type (u,utab) s = try type_of_typed_entry (Hashtbl.find utab s) with Not_found -> - error ("unknown grammar entry "^u^":"^s) + error ("Unknown grammar entry "^u^":"^s^".") let force_entry_type (u, utab) s etyp = try @@ -578,7 +578,7 @@ let error_level_assoc p current expected = errorlabstrm "" (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ - pr_assoc expected ++ str " associative") + pr_assoc expected ++ str " associative.") let find_position_gen forpat ensure assoc lev = let ccurrent,pcurrent as current = List.hd !level_stack in @@ -695,7 +695,7 @@ let compute_entry allow_create adjust forpat = function | ETPattern -> weaken_entry Constr.pattern, None, false | ETOther ("constr","annot") -> weaken_entry Constr.annot, None, false - | ETConstrList _ -> error "List of entries cannot be registered" + | ETConstrList _ -> error "List of entries cannot be registered." | ETOther (u,n) -> let u = get_univ u in let e = @@ -762,6 +762,6 @@ let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> user_err_loc (loc, "coerce_reference_to_id", - str "This expression should be a simple identifier") + str "This expression should be a simple identifier.") let coerce_global_to_id = coerce_reference_to_id diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 912406f3f..ca8b97588 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -719,7 +719,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function hov 1 (str "pattern" ++ pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l) - | Red true -> error "Shouldn't be accessible from user" + | Red true -> error "Shouldn't be accessible from user." | ExtraRedExpr s -> str s | CbvVm -> str "vm_compute" diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3d1eec4fe..2a0e755ff 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -58,7 +58,7 @@ let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) = let s = match unquote wit with | ExtraArgType s -> s | _ -> error - "Can declare a pretty-printing rule only for extra argument types" + "Can declare a pretty-printing rule only for extra argument types." in let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index bdbd74b0f..0a9447b46 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -219,7 +219,7 @@ let pr_located_qualid = function | ModuleType (qid,_) -> str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid) | Undefined qid -> - pr_qualid qid ++ str " is not a defined object" + pr_qualid qid ++ spc () ++ str "not a defined object." let print_located_qualid ref = let (loc,qid) = qualid_of_reference ref in @@ -599,12 +599,12 @@ let read_sec_context r = let dir = try Nametab.locate_section qid with Not_found -> - user_err_loc (loc,"read_sec_context", str "Unknown section") in + user_err_loc (loc,"read_sec_context", str "Unknown section.") in let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if 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" + error "Cannot print the contents of a closed section." (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest @@ -648,7 +648,7 @@ let print_name ref = print_leaf_entry true (oname,lobj) with Not_found -> errorlabstrm - "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object") + "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") let print_opaque_name qid = let env = Global.env () in @@ -658,7 +658,7 @@ let print_opaque_name qid = if cb.const_body <> None then print_constant_with_infos cst else - error "not a defined constant" + error "Not a defined constant." | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr -> @@ -736,7 +736,8 @@ let index_of_class cl = try fst (class_info cl) with _ -> - errorlabstrm "index_of_class" (pr_class cl ++ str" is not a defined class") + errorlabstrm "index_of_class" + (pr_class cl ++ spc() ++ str "not a defined class.") let print_path_between cls clt = let i = index_of_class cls in @@ -746,7 +747,8 @@ let print_path_between cls clt = lookup_path_between (i,j) with _ -> errorlabstrm "index_cl_of_id" - (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt) + (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt + ++ str ".") in print_path ((i,j),p) diff --git a/parsing/printer.ml b/parsing/printer.ml index 6119f5d1e..f59f9f2f3 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -318,7 +318,7 @@ let rec pr_evars_int i = function let default_pr_subgoal n = let rec prrec p = function - | [] -> error "No such goal" + | [] -> error "No such goal." | g::rest -> if p = 1 then let pg = default_pr_goal g in diff --git a/parsing/search.ml b/parsing/search.ml index 88b51907b..9670c2b87 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -150,7 +150,7 @@ let rec id_from_pattern = function | PVar id -> Nametab.locate (make_qualid [] (string_of_id id)) *) | PApp (p,_) -> id_from_pattern p - | _ -> error "the pattern is not simple enough" + | _ -> error "The pattern is not simple enough." let raw_pattern_search extra_filter display_function pat = let name = id_from_pattern pat in diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 6e8425d98..65b3a075e 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -206,7 +206,7 @@ EXTEND let t, g = Q_util.interp_entry_name loc e sep in TacNonTerm (loc, t, g, Some s) | s = STRING -> - if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal"); + if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal."); TacTerm s ] ] ; diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 0b3dd75ad..29e30bca7 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -110,7 +110,7 @@ EXTEND rule: [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]" -> - if s = "" then Util.user_err_loc (loc,"",Pp.str "Command name is empty"); + if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty."); (s,l,<:expr< fun () -> $e$ >>) ] ] ; diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 52c8ca419..3839561bf 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -114,8 +114,8 @@ let force_name = open Pp -let mssg_may_need_inversion () = - str "Found a matching with no clauses on a term unknown to have an empty inductive type" +let msg_may_need_inversion () = + strbrk "Found a matching with no clauses on a term unknown to have an empty inductive type." (* Utils *) let make_anonymous_patvars n = @@ -535,7 +535,7 @@ let set_used_pattern eqn = eqn.used := true let extract_rhs pb = match pb.mat with - | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion()) + | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion()) | eqn::_ -> set_used_pattern eqn; eqn.rhs @@ -1654,7 +1654,7 @@ let extract_arity_signature env0 tomatchl tmsign = | None -> [na,Option.map (lift n) bo,lift n typ] | Some (loc,_,_,_) -> user_err_loc (loc,"", - str "Unexpected type annotation for a term of non inductive type")) + str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = lift_inductive_family n indf in let (ind,params) = dest_ind_family indf' in @@ -1663,7 +1663,7 @@ let extract_arity_signature env0 tomatchl tmsign = match t with | Some (loc,ind',nparams,realnal) -> if ind <> ind' then - user_err_loc (loc,"",str "Wrong inductive type"); + user_err_loc (loc,"",str "Wrong inductive type."); if List.length params <> nparams or nrealargs <> List.length realnal then anomaly "Ill-formed 'in' clause in cases"; diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 0d7e3d611..0ffaed371 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -376,7 +376,7 @@ let coercion_of_reference r = let ref = Nametab.global r in if not (coercion_exists ref) then errorlabstrm "try_add_coercion" - (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion"); + (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion."); ref module CoercionPrinting = diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index c91580044..732ff1e69 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -377,11 +377,11 @@ let check_bindings bl = | NamedHyp s :: _ -> errorlabstrm "" (str "The variable " ++ pr_id s ++ - str " occurs more than once in binding list"); + str " occurs more than once in binding list."); | AnonHyp n :: _ -> errorlabstrm "" (str "The position " ++ int n ++ - str " occurs more than once in binding list") + str " occurs more than once in binding list.") | [] -> () let meta_of_binder clause loc mvs = function @@ -389,17 +389,17 @@ let meta_of_binder clause loc mvs = function | AnonHyp n -> try List.nth mvs (n-1) with (Failure _|Invalid_argument _) -> - errorlabstrm "" (str "No such binder") + errorlabstrm "" (str "No such binder.") let error_already_defined b = match b with | NamedHyp id -> errorlabstrm "" (str "Binder name \"" ++ pr_id id ++ - str"\" already defined with incompatible value") + str"\" already defined with incompatible value.") | AnonHyp n -> anomalylabstrm "" - (str "Position " ++ int n ++ str" already defined") + (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = if isMeta (fst (whd_stack u)) then @@ -440,7 +440,7 @@ let clenv_constrain_last_binding c clenv = let all_mvs = collect_metas clenv.templval.rebus in let k = try list_last all_mvs - with Failure _ -> error "clenv_constrain_with_bindings" in + with Failure _ -> anomaly "clenv_constrain_with_bindings" in clenv_assign_binding clenv k (Evd.empty,c) let clenv_constrain_dep_args hyps_only bl clenv = @@ -451,8 +451,9 @@ let clenv_constrain_dep_args hyps_only bl clenv = if List.length occlist = List.length bl then List.fold_left2 clenv_assign_binding clenv occlist bl else - error ("Not the right number of missing arguments (expected " - ^(string_of_int (List.length occlist))^")") + errorlabstrm "" + (strbrk "Not the right number of missing arguments (expected " ++ + int (List.length occlist) ++ str ").") (****************************************************************) (* Clausal environment for an application *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8d8a9950e..6854a4a7c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -49,14 +49,14 @@ let encode_bool r = let (_,lc as x) = encode_inductive r in if not (has_two_constructors lc) then user_err_loc (loc_of_reference r,"encode_if", - str "This type has not exactly two constructors"); + str "This type has not exactly two constructors."); x let encode_tuple r = let (_,lc as x) = encode_inductive r in if not (isomorphic_to_tuple lc) then user_err_loc (loc_of_reference r,"encode_tuple", - str "This type cannot be seen as a tuple type"); + str "This type cannot be seen as a tuple type."); x module PrintingCasesMake = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 1463901a5..cd09691d0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -505,7 +505,7 @@ let choose_less_dependent_instance evk evd term args = let evi = Evd.find (evars_of evd) evk in let subst = make_pure_subst evi args in let subst' = List.filter (fun (id,c) -> c = term) subst in - if subst' = [] then error "Too complex unification problem" else + if subst' = [] then error "Too complex unification problem." else Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd let apply_conversion_problem_heuristic env evd pbty t1 t2 = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 870debaa7..2f2665bbc 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -451,8 +451,9 @@ let clear_hyps_in_evi evdref hyps concl ids = None -> None | Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)), check_and_clear_in_constr evdref c ids EvkSet.empty) - with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis " - ^ string_of_id id) + with Dependency_error id' -> + errorlabstrm "" (pr_id id' ++ strbrk " is used in hypothesis " + ++ pr_id id ++ str ".") in let check_value vk = match !vk with @@ -883,7 +884,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = and evar_define env (evk,_ as ev) rhs evd = try let (evd',body) = invert_definition env evd ev rhs in - if occur_meta body then error "Meta cannot occur in evar body"; + if occur_meta body then error "Meta cannot occur in evar body."; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) if occur_evar evk body then error_occur_check env (evars_of evd) evk body; diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 166114ab6..ecc63ce94 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -598,13 +598,13 @@ let meta_with_name evd id = match mvnodef, mvl with | _,[] -> errorlabstrm "Evd.meta_with_name" - (str"No such bound variable " ++ pr_id id) + (str"No such bound variable " ++ pr_id id ++ str".") | ([n],_|_,[n]) -> n | _ -> errorlabstrm "Evd.meta_with_name" (str "Binder name \"" ++ pr_id id ++ - str"\" occurs more than once in clause") + strbrk "\" occurs more than once in clause.") let meta_merge evd1 evd2 = diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 37d60e470..ffbc9debc 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -591,12 +591,10 @@ let lookup_eliminator ind_sp s = try constr_of_global (Nametab.locate (make_short_qualid id)) with Not_found -> errorlabstrm "default_elim" - (str "Cannot find the elimination combinator " ++ - pr_id id ++ spc () ++ - str "The elimination of the inductive definition " ++ - pr_id id ++ spc () ++ str "on sort " ++ - spc () ++ pr_sort_family s ++ - str " is probably not allowed") + (strbrk "Cannot find the elimination combinator " ++ + pr_id id ++ strbrk ", the elimination of the inductive definition " ++ + pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++ + strbrk " is probably not allowed.") (* let env = Global.env() in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 66f345643..79d9e381e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -87,7 +87,7 @@ let mis_nf_constructor_type (ind,mib,mip) j = and ntypes = mib.mind_ntypes and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkInd ((fst ind),ntypes-k-1) in - if j > nconstr then error "Not enough constructors in the type"; + if j > nconstr then error "Not enough constructors in the type."; substl (list_tabulate make_Ik ntypes) specif.(j-1) (* Arity of constructors excluding parameters and local defs *) diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 6b3b4e175..9a3130605 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -110,7 +110,7 @@ let matches_core convert allow_partial_app pat c = List.map (function | PRel n -> n - | _ -> error "Only bound indices allowed in second order pattern matching") + | _ -> error "Only bound indices allowed in second order pattern matching.") args in let frels = Intset.elements (free_rels cT) in if list_subset frels relargs then diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 05af1652e..ba53d127e 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -133,7 +133,7 @@ let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) () let rec instantiate_pattern lvar = function | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x) - | (PFix _ | PCoFix _) -> error ("Not instantiable pattern") + | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") | c -> map_pattern (instantiate_pattern lvar) c let rec liftn_pattern k n = function @@ -264,7 +264,7 @@ let rec pat_of_raw metas vars = function | r -> let loc = loc_of_rawconstr r in - user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported") + user_err_loc (loc,"pattern_of_rawconstr", Pp.str"Non supported pattern.") and pat_of_raw_branch loc metas vars ind brs i = let bri = List.filter @@ -272,23 +272,23 @@ and pat_of_raw_branch loc metas vars ind brs i = (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1 | (loc,_,_,_) -> user_err_loc (loc,"pattern_of_rawconstr", - Pp.str "Not supported pattern")) brs in + Pp.str "Non supported pattern.")) brs in match bri with | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] -> if ind <> None & ind <> Some indsp then user_err_loc (loc,"pattern_of_rawconstr", - Pp.str "All constructors must be in the same inductive type"); + Pp.str "All constructors must be in the same inductive type."); let lna = List.map (function PatVar(_,na) -> na | PatCstr(loc,_,_,_) -> user_err_loc (loc,"pattern_of_rawconstr", - Pp.str "Not supported pattern")) lv in + Pp.str "Non supported pattern.")) lv in let vars' = List.rev lna @ vars in List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br) | _ -> user_err_loc (loc,"pattern_of_rawconstr", str "No unique branch for " ++ int (i+1) ++ - str"-th constructor") + str"-th constructor.") let pattern_of_rawconstr c = let metas = ref [] in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 17c7efb45..08ecae12e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -66,7 +66,7 @@ let search_guard loc env possible_indexes fixdefs = try check_fix env fix; raise (Found indexes) with TypeError _ -> ()) (list_combinations possible_indexes); - let errmsg = "cannot guess decreasing argument of fix" in + let errmsg = "Cannot guess decreasing argument of fix." in if loc = dummy_loc then error errmsg else user_err_loc (loc,"search_guard", Pp.str errmsg) with Found indexes -> indexes) @@ -244,7 +244,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct try (* To build a nicer ltac error message *) match List.assoc id unbndltacvars with | None -> user_err_loc (loc,"", - str "variable " ++ pr_id id ++ str " should be bound to a term") + str "Variable " ++ pr_id id ++ str " should be bound to a term.") | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> error_var_not_found_loc loc id @@ -461,10 +461,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct in let cstrs = get_constructors env indf in if Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); + user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor."); let cs = cstrs.(0) in if List.length nal <> cs.cs_nargs then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); + user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) (List.rev nal) cs.cs_args in let env_f = push_rels fsign env in @@ -527,7 +527,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let cstrs = get_constructors env indf in if Array.length cstrs <> 2 then user_err_loc (loc,"", - str "If is only for inductive types with two constructors"); + str "If is only for inductive types with two constructors."); let arsgn = let arsgn,_ = get_arity env indf in @@ -615,7 +615,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct j (*inh_conv_coerce_to_tycon loc env evdref j tycon*) else - user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic")) + user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic.")) (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type valcon env evdref lvar = function diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7dbbf9933..100109652 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -217,7 +217,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref = errorlabstrm "object_declare" - (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object") + (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object.") let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 055d2e51b..12594dd6d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -773,7 +773,7 @@ let splay_arity env sigma c = let l, c = splay_prod env sigma c in match kind_of_term c with | Sort s -> l,s - | _ -> error "not an arity" + | _ -> invalid_arg "splay_arity" let sort_of_arity env c = snd (splay_arity env Evd.empty c) @@ -783,7 +783,7 @@ let decomp_n_prod env sigma n = | Prod (n,a,c0) -> decrec (push_rel (n,None,a) env) (m-1) (Sign.add_rel_decl (n,None,a) ln) c0 - | _ -> error "decomp_n_prod: Not enough products" + | _ -> invalid_arg "decomp_n_prod" in decrec env n Sign.empty_rel_context diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 47bc132ac..0dd94d813 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -543,7 +543,7 @@ let try_red_product env sigma c = let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "Not reducible" + with Redelimination -> error "Not reducible." (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -698,7 +698,7 @@ let unfold env sigma name = if is_evaluable env name then clos_norm_flags (unfold_red name) env sigma else - error (string_of_evaluable_ref env name^" is opaque") + error (string_of_evaluable_ref env name^" is opaque.") (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. @@ -709,7 +709,7 @@ let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c = else let (nbocc,uc) = substlin env name 1 plocs c in if nbocc = 1 then - error ((string_of_evaluable_ref env name)^" does not occur"); + error ((string_of_evaluable_ref env name)^" does not occur."); let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest; nf_betaiota uc @@ -722,7 +722,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 -> error "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 *) @@ -757,7 +757,7 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) c = let ta = Retyping.get_type_of env sigma a in let na = named_hd env ta Anonymous in - if occur_meta ta then error "cannot find a type for the generalisation"; + if occur_meta ta then error "Cannot find a type for the generalisation."; if occur_meta a then mkLambda (na,ta,c) else @@ -785,14 +785,14 @@ let reduce_to_ind_gen allow_product env sigma t = if allow_product then elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l) else - errorlabstrm "" (str"Not an inductive definition") + errorlabstrm "" (str"Not an inductive definition.") | _ -> (* Last chance: we allow to bypass the Opaque flag (as it was partially the case between V5.10 and V8.1 *) let t' = whd_betadeltaiota env sigma t in match kind_of_term (fst (decompose_app t')) with | Ind ind-> (ind, it_mkProd_or_LetIn t' l) - | _ -> errorlabstrm "" (str"Not an inductive product") + | _ -> errorlabstrm "" (str"Not an inductive product.") in elimrec env t [] @@ -843,7 +843,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = let (mind,t) = reduce_to_ind_gen allow_product env sigma t in if IndRef mind <> ref then errorlabstrm "" (str "Cannot recognize a statement based on " ++ - Nametab.pr_global_env Idset.empty ref) + Nametab.pr_global_env Idset.empty ref ++ str".") else t else @@ -857,7 +857,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = else errorlabstrm "" (str "Cannot recognize an atomic statement based on " ++ - Nametab.pr_global_env Idset.empty ref) + Nametab.pr_global_env Idset.empty ref ++ str".") | _ -> try if global_of_constr c = ref @@ -870,7 +870,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = with NotStepReducible -> errorlabstrm "" (str "Cannot recognize a statement based on " ++ - Nametab.pr_global_env Idset.empty ref) + Nametab.pr_global_env Idset.empty ref ++ str".") in elimrec env t [] diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 4246f0daa..22090d88c 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -639,7 +639,7 @@ let error_invalid_occurrence l = let l = list_uniquize (List.sort Pervasives.compare l) in errorlabstrm "" (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ - prlist_with_sep spc int l) + prlist_with_sep spc int l ++ str ".") let subst_term_occ_gen (nowhere_except_in,locs) occ c t = let maxocc = List.fold_right max locs 0 in diff --git a/tactics/auto.ml b/tactics/auto.ml index dfc9a6ad2..1c3e2ce08 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -220,7 +220,7 @@ let rec nb_hyp c = match kind_of_term c with let try_head_pattern c = try head_pattern_bound c - with BoundPattern -> error "Bound head variable" + with BoundPattern -> error "Bound head variable." let dummy_goal = {it = make_evar empty_named_context_val mkProp; @@ -279,8 +279,8 @@ let make_resolves env sigma flags pri c = if ents = [] then errorlabstrm "Hint" (pr_lconstr c ++ spc() ++ - (if fst flags then str"cannot be used as a hint" - else str "can be used as a hint only for eauto")); + (if fst flags then str"cannot be used as a hint." + else str "can be used as a hint only for eauto.")); ents (* used to add an hypothesis to the local hint database *) @@ -438,7 +438,7 @@ let add_extern pri (patmetas,pat) tacast local dbname = match (list_subtract tacmetas patmetas) with | i::_ -> errorlabstrm "add_extern" - (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound") + (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") | [] -> Lib.add_anonymous_leaf (inAutoHint(local,dbname, UpdateDB [make_extern pri pat tacast])) @@ -476,7 +476,7 @@ let add_hints local dbnames0 h = | _ -> errorlabstrm "evalref_of_ref" (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ - str "to an evaluable reference") + str "to an evaluable reference.") in if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr; (gr,r') in @@ -571,6 +571,9 @@ let fmt_hint_term cl = hov 0 (prlist fmt_hints_db valid_dbs)) with Bound | Match_failure _ | Failure _ -> (str "No hint applicable for current goal") + +let error_no_such_hint_database x = + error ("No such Hint database: "^x^".") let print_hint_term cl = ppnl (fmt_hint_term cl) @@ -597,13 +600,13 @@ let print_hint_db_by_name dbname = try let db = searchtable_map dbname in print_hint_db db with Not_found -> - error (dbname^" : No such Hint database") + error_no_such_hint_database dbname (* displays all the hints of all databases *) let print_searchtable () = Hintdbmap.iter (fun name db -> - msg (str "In the database " ++ str name ++ fnl ()); + msg (str "In the database " ++ str name ++ str ":" ++ fnl ()); print_hint_db db) !searchtable @@ -774,7 +777,7 @@ let trivial lems dbnames gl = try searchtable_map x with Not_found -> - error ("trivial: "^x^": No such Hint database")) + error_no_such_hint_database x) ("core"::dbnames) in tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl @@ -813,7 +816,7 @@ let decomp_unary_term c gls = if Hipattern.is_conjunction hd then simplest_case c gls else - errorlabstrm "Auto.decomp_unary_term" (str "not a unary type") + errorlabstrm "Auto.decomp_unary_term" (str "Not a unary type.") let decomp_empty_term c gls = let typc = pf_type_of gls c in @@ -821,7 +824,7 @@ let decomp_empty_term c gls = if Hipattern.is_empty_type hd then simplest_case c gls else - errorlabstrm "Auto.decomp_empty_term" (str "not an empty type") + errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.") (* decomp is an natural number giving an indication on decomposition @@ -877,7 +880,7 @@ let delta_auto mod_delta n lems dbnames gl = try searchtable_map x with Not_found -> - error ("auto: "^x^": No such Hint database")) + error_no_such_hint_database x) ("core"::dbnames) in let hyps = pf_hyps gl in diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 3be1e45de..68c61bca0 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -56,7 +56,7 @@ let print_rewrite_hintdb bas = with Not_found -> errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist")) + (str ("Rewriting base "^(bas)^" does not exist.")) type raw_rew_rule = constr * bool * raw_tactic_expr @@ -67,7 +67,7 @@ let one_base general_rewrite_maybe_in tac_main bas = Stringmap.find bas !rewtab with Not_found -> errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist")) + (str ("Rewriting base "^(bas)^" does not exist.")) in let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) -> @@ -99,7 +99,7 @@ let autorewrite_multi_in idl tac_main lbas : tactic = match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with (last_hyp_id,_,_)::_ -> last_hyp_id | _ -> (* even the hypothesis id is missing *) - error ("No such hypothesis : " ^ (string_of_id !id)) + error ("No such hypothesis: " ^ (string_of_id !id) ^".") in let gl' = general_rewrite_in dir all_occurrences !id cstr false gl in let gls = (fst gl').Evd.it in @@ -140,7 +140,7 @@ let gen_auto_multi_rewrite tac_main lbas cl = if cl.concl_occs <> all_occurrences_expr & cl.concl_occs <> no_occurrences_expr then - error "The \"at\" syntax isn't available yet for the autorewrite tactic" + error "The \"at\" syntax isn't available yet for the autorewrite tactic." else let compose_tac t1 t2 = match cl.onhyps with @@ -170,8 +170,7 @@ let auto_multi_rewrite_with tac_main lbas cl gl = gen_auto_multi_rewrite tac_main lbas cl gl | _ -> Util.errorlabstrm "autorewrite" - (str "autorewrite .. in .. using can only be used either with a unique hypothesis or" ++ - str " on the conclusion") + (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") (* Functions necessary to the library object declaration *) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 6312cefc1..700ce5895 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -49,7 +49,7 @@ let check_imported_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in if not (Library.library_is_loaded dir) then - error ("Library "^(list_last d)^" has to be imported first") + error ("Library "^(list_last d)^" has to be imported first.") let classes_dirpath = make_dirpath (List.map id_of_string ["Classes";"Coq"]) @@ -354,7 +354,7 @@ let e_breadth_search debug s = let tac = if debug then Search.debug_breadth_first else Search.breadth_first in let s = tac s in s.tacres - with Not_found -> error "EAuto: breadth first search failed" + with Not_found -> error "eauto: breadth first search failed." let e_search_auto debug (in_depth,p) lems st db_list gls = let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in @@ -727,13 +727,13 @@ let decompose_setoid_eqhyp env sigma c left2right = | [c1;c2] -> [],(c1, c2) | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "The term provided is not an applied relation" in + | _ -> error "The term provided is not an applied relation." in let others,(c1,c2) = split_last_two args in let ty1, ty2 = Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2 in if not (evd_convertible env eqclause.evd ty1 ty2) then - error "The term does not end with an applied homogeneous relation" + error "The term does not end with an applied homogeneous relation." else { cl=eqclause; prf=(Clenv.clenv_value eqclause); car=ty1; rel=mkApp (equiv, Array.of_list others); @@ -1102,7 +1102,7 @@ let occurrences_of = function | n::_ as nl when n < 0 -> (false,List.map abs nl) | nl -> if List.exists (fun n -> n < 0) nl then - error "Illegal negative occurrence number"; + error "Illegal negative occurrence number."; (true,nl) TACTIC EXTEND class_rewrite @@ -1609,7 +1609,7 @@ let relation_of_constr c = | App (f, args) when Array.length args >= 2 -> let relargs, args = array_chop (Array.length args - 2) args in mkApp (f, relargs), args - | _ -> error "Not an applied relation" + | _ -> error "Not an applied relation." let is_loaded d = let d' = List.map id_of_string d in @@ -1656,7 +1656,7 @@ let setoid_symmetry_in id gl = 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 "The term provided is not an equivalence" + | _ -> error "The term provided is not an equivalence." 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/tactics/contradiction.ml b/tactics/contradiction.ml index 535fd6632..4b48064b3 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -85,7 +85,7 @@ let contradiction_term (c,lbind as cl) gl = (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl else raise Not_found - with Not_found -> error "Not a contradiction" + with Not_found -> error "Not a contradiction." let contradiction = function | None -> tclTHEN intros contradiction_context diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 4eb59a2fb..a25fcd923 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id$ i*) open Util open Names @@ -162,8 +162,8 @@ let decompose_eq env id = App (f,args)-> if eq_constr f _eq && (Array.length args)=3 then args.(0) - else error "previous step is not an equality" - | _ -> error "previous step is not an equality" + else error "Previous step is not an equality." + | _ -> error "Previous step is not an equality." let get_eq_typ info env = let typ = decompose_eq env (get_last env) in @@ -331,9 +331,9 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let expected = mib.Declarations.mind_nparams - num_params in if List.length params <> expected then errorlabstrm "suppose it is" - (str "Wrong number of extra arguments : " ++ + (str "Wrong number of extra arguments: " ++ (if expected = 0 then str "none" else int expected) ++ - str "expected") in + str "expected.") in let app_ind = let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in let rparams = List.map detype_ground pinfo.per_params in @@ -400,7 +400,7 @@ let interp_suffices_clause sigma env (hyps,cot)= let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in nhyps,This nc | Thesis Plain as th -> interp_hyps sigma env hyps,th - | Thesis (For n) -> error "\"thesis for\" is not applicable here" in + | Thesis (For n) -> error "\"thesis for\" is not applicable here." in let push_one hyp env0 = match hyp with (Hprop st | Hvar st) -> diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 133524ba7..cbb8996f6 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -188,7 +188,7 @@ let close_tactic_mode pts = let pts1= try goto_current_focus pts with Not_found -> - error "\"return\" cannot be used outside of Declarative Proof Mode" in + error "\"return\" cannot be used outside of Declarative Proof Mode." in let pts2 = daimon_subtree pts1 in let pts3 = mark_as_done pts2 in goto_current_focus pts3 @@ -207,18 +207,18 @@ let close_block bt pts = B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> daimon_subtree (goto_current_focus pts) | _, Claim::_ -> - error "\"end claim\" expected" + error "\"end claim\" expected." | _, Focus_claim::_ -> - error "\"end focus\" expected" + error "\"end focus\" expected." | _, [] -> - error "\"end proof\" expected" + error "\"end proof\" expected." | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) -> begin match et with - ET_Case_analysis -> error "\"end cases\" expected" - | ET_Induction -> error "\"end induction\" expected" + ET_Case_analysis -> error "\"end cases\" expected." + | ET_Induction -> error "\"end induction\" expected." end - | _,_ -> anomaly "lonely suppose on stack" + | _,_ -> anomaly "Lonely suppose on stack." (* utility for suppose / suppose it is *) @@ -284,10 +284,10 @@ let justification tac gls= (tclSOLVE [tclTHEN tac assumption]) (fun gls -> if get_strictness () then - error "insufficient justification" + error "Insufficient justification." else begin - msg_warning (str "insufficient justification"); + msg_warning (str "Insufficient justification."); daimon_tac gls end) gls @@ -475,7 +475,7 @@ let thus_tac c ctyp submetas gls = try find_subsubgoal c ctyp 0 submetas gls with Not_found -> - error "I could not relate this statement to the thesis" in + error "I could not relate this statement to the thesis." in if list = [] then exact_check proof gls else @@ -490,7 +490,7 @@ let anon_id_base = id_of_string "__" let mk_stat_or_thesis info gls = function This c -> c | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here" + error "\"thesis for ...\" is not applicable here." | Thesis Plain -> pf_concl gls let just_tac _then cut info gls0 = @@ -542,12 +542,12 @@ let decompose_eq id gls = then (args.(0), args.(1), args.(2)) - else error "previous step is not an equality" - | _ -> error "previous step is not an equality" + else error "Previous step is not an equality." + | _ -> error "Previous step is not an equality." let instr_rew _thus rew_side cut gls0 = let last_id = - try get_last (pf_env gls0) with _ -> error "no previous equality" in + try get_last (pf_env gls0) with _ -> error "No previous equality." in let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = match cut.cut_by with @@ -730,7 +730,7 @@ let rec consider_match may_intro introduced available expected gls = match available,expected with [],[] -> tclIDTAC gls - | _,[] -> error "last statements do not match a complete hypothesis" + | _,[] -> error "Last statements do not match a complete hypothesis." (* should tell which ones *) | [],hyps -> if may_intro then @@ -740,11 +740,11 @@ let rec consider_match may_intro introduced available expected gls = (intro_mustbe_force id) (consider_match true [] [id] hyps) (fun _ -> - error "not enough sub-hypotheses to match statements") + error "Not enough sub-hypotheses to match statements.") gls end else - error "not enough sub-hypotheses to match statements" + error "Not enough sub-hypotheses to match statements." (* should tell which ones *) | id::rest_ids,(Hvar st | Hprop st)::rest -> tclIFTHENELSE (convert_hyp (id,None,st.st_it)) @@ -761,7 +761,7 @@ let rec consider_match may_intro introduced available expected gls = (fun gls -> let nhyps = try conjunction_arity id gls with - Not_found -> error "matching hypothesis not found" in + Not_found -> error "Matching hypothesis not found." in tclTHENLIST [general_case_analysis false (mkVar id,NoBindings); intron_then nhyps [] @@ -818,7 +818,7 @@ let cast_tac id_or_thesis typ gls = let (_,body,_) = pf_get_hyp gls id in convert_hyp (id,body,typ) gls | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here" + error "\"thesis for ...\" is not applicable here." | Thesis Plain -> convert_concl typ DEFAULTcast gls @@ -884,7 +884,7 @@ let build_per_info etype casee gls = try destInd hd with _ -> - error "Case analysis must be done on an inductive object" in + error "Case analysis must be done on an inductive object." in let mind,oind = Global.lookup_inductive ind in let nparams,index = match etype with @@ -1042,7 +1042,7 @@ let rec add_branch ((id,_) as cpl) pats tree= | Split_patt (_,ind0,_) -> if (ind <> ind0) then error (* this can happen with coercions *) - "Case pattern belongs to wrong inductive type"; + "Case pattern belongs to wrong inductive type."; let mapi i ati bri = if i = pred cnum then let nargs = @@ -1083,12 +1083,12 @@ let thesis_for obj typ per_info env= let _ = if ind <> per_info.per_ind then errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ - str "cannot give an induction hypothesis (wrong inductive type)") in + str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = list_chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ - str "cannot give an induction hypothesis (wrong parameters)") in + str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in compose_prod rc (whd_beta hd2) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 7d2ccbe21..80b505a00 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -246,7 +246,7 @@ let add_destructor_hint local na loc pat pri code = | ConclLocation _, _ -> (None, code) | _ -> errorlabstrm "add_destructor_hint" - (str "The tactic should be a function of the hypothesis name") end + (str "The tactic should be a function of the hypothesis name.") end in let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat in @@ -279,13 +279,13 @@ let match_dpat dp cls gls = (is_matching concld.d_typ cl) & (is_matching concld.d_sort (pf_type_of gls cl))) hl) - then error "No match" + then error "No match." | ({onhyps=Some[]},ConclLocation concld) when onconcl -> let cl = pf_concl gls in if not ((is_matching concld.d_typ cl) & (is_matching concld.d_sort (pf_type_of gls cl))) - then error "No match" + then error "No match." | _ -> error "ApplyDestructor" let forward_interp_tactic = @@ -304,8 +304,8 @@ let applyDestructor cls discard dd gls = ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in TacLetIn (false, [(dummy_loc, x), arg], tac) | None, (None, tac) -> tac - | _, (Some _,_) -> error "Destructor expects an hypothesis" - | _, (None,_) -> error "Destructor is for conclusion") + | _, (Some _,_) -> error "Destructor expects an hypothesis." + | _, (None,_) -> error "Destructor is for conclusion.") cll in let discard_0 = List.map (fun cl -> diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 70bc9a592..eae6f5632 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -74,11 +74,11 @@ let prolog_tac l n gl = let n = match n with | ArgArg n -> n - | _ -> error "Prolog called with a non closed argument" + | _ -> error "Prolog called with a non closed argument." in try (prolog l n gl) with UserError ("Refiner.tclFIRST",_) -> - errorlabstrm "Prolog.prolog" (str "Prolog failed") + errorlabstrm "Prolog.prolog" (str "Prolog failed.") TACTIC EXTEND prolog | [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ] @@ -331,7 +331,7 @@ let e_depth_search debug p db_list local_db gl = let tac = if debug then Search.debug_depth_first else Search.depth_first in let s = tac (make_initial_state p gl db_list local_db) in s.tacres - with Not_found -> error "EAuto: depth first search failed" + with Not_found -> error "eauto: depth first search failed." let e_breadth_search debug n db_list local_db gl = try @@ -340,7 +340,7 @@ let e_breadth_search debug n db_list local_db gl = in let s = tac (make_initial_state n gl db_list local_db) in s.tacres - with Not_found -> error "EAuto: breadth first search failed" + with Not_found -> error "eauto: breadth first search failed." let e_search_auto debug (in_depth,p) lems db_list gl = let local_db = make_local_hint_db true lems gl in @@ -359,7 +359,7 @@ let eauto debug np lems dbnames = List.map (fun x -> try searchtable_map x - with Not_found -> error ("EAuto: "^x^": No such Hint database")) + with Not_found -> error ("No such Hint database: "^x^".")) ("core"::dbnames) in tclTRY (e_search_auto debug np lems db_list) @@ -377,12 +377,12 @@ let gen_eauto d np lems = function let make_depth = function | None -> !default_search_depth | Some (ArgArg d) -> d - | _ -> error "EAuto called with a non closed argument" + | _ -> error "eauto called with a non closed argument." let make_dimension n = function | None -> (true,make_depth n) | Some (ArgArg d) -> (false,d) - | _ -> error "EAuto called with a non closed argument" + | _ -> error "eauto called with a non closed argument." open Genarg diff --git a/tactics/elim.ml b/tactics/elim.ml index 43ea91f5a..f0cc50d49 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -115,7 +115,7 @@ let inductive_of = function | IndRef ity -> ity | r -> errorlabstrm "Decompose" - (Printer.pr_global r ++ str " is not an inductive type") + (Printer.pr_global r ++ str " is not an inductive type.") let decompose_these c l gls = let indl = (*List.map inductive_of*) l in @@ -182,7 +182,7 @@ let double_ind h1 h2 gls = let (abs_i,abs_j) = if abs_i < abs_j then (abs_i,abs_j) else if abs_i > abs_j then (abs_j,abs_i) else - error "Both hypotheses are the same" in + error "Both hypotheses are the same." in (tclTHEN (tclDO abs_i intro) (onLastHyp (fun id -> diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 61100f0a5..625a09662 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -152,14 +152,14 @@ let decideGralEquality g = let rectype = match kind_of_term headtyp with | Ind mi -> mi - | _ -> error "This decision procedure only works for inductive objects" + | _ -> error"This decision procedure only works for inductive objects." in (tclTHEN (mkBranches c1 c2) (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype))) g with PatternMatchingFailure -> - error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}" + error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}." let decideEqualityGoal = tclTHEN intros decideGralEquality diff --git a/tactics/equality.ml b/tactics/equality.ml index 329284136..8831a9e57 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -97,7 +97,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl = | None -> if l = NoBindings then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl - else error "The term provided does not end with an equation" + else error "The term provided does not end with an equation." | Some (hdcncl,_) -> if occs <> all_occurrences then ( !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl) @@ -109,7 +109,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl = let elim = try pf_global gl (id_of_string rwr_thm) with Not_found -> - error ("Cannot find rewrite principle "^rwr_thm) + error ("Cannot find rewrite principle "^rwr_thm^".") in try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl with e -> @@ -258,7 +258,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = ] ] gl else - error "terms do not have convertible types" + error "Terms do not have convertible types." let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl @@ -483,7 +483,7 @@ let construct_discriminator sigma env dirn c sort = *) errorlabstrm "Equality.construct_discriminator" (str "Cannot discriminate on inductive constructors with - dependent types") in + dependent types.") in let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in @@ -523,7 +523,7 @@ let gen_absurdity id gl = simplest_elim (mkVar id) gl else errorlabstrm "Equality.gen_absurdity" - (str "Not the negation of an equality") + (str "Not the negation of an equality.") (* Precondition: eq is leibniz equality @@ -548,7 +548,7 @@ let apply_on_clause (f,t) clause = let argmv = (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> errorlabstrm "" (str "Ill-formed clause applicator")) in + | _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in clenv_fchain argmv f_clause clause let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort = @@ -569,7 +569,7 @@ let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls = let env = pf_env gls in match find_positions env sigma t1 t2 with | Inr _ -> - errorlabstrm "discr" (str"Not a discriminable equality") + errorlabstrm "discr" (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> let sort = pf_apply get_type_of gls (pf_concl gls) in discr_positions env sigma u eq_clause cpath dirn sort gls @@ -583,7 +583,7 @@ let onEquality with_evars tac (c,lbindc) gls = let eq = try find_eq_data_decompose eqn with PatternMatchingFailure -> - errorlabstrm "" (str"No primitive equality found") in + errorlabstrm "" (str"No primitive equality found.") in tclTHEN (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) (tac eq eq_clause') gls @@ -596,7 +596,7 @@ let onNegatedEquality with_evars tac gls = (onLastHyp (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) gls | _ -> - errorlabstrm "" (str "Not a negated primitive equality") + errorlabstrm "" (str "Not a negated primitive equality.") let discrSimpleClause with_evars = function | None -> onNegatedEquality with_evars discrEq @@ -613,7 +613,7 @@ let discrEverywhere with_evars = (Tacticals.tryAllHyps (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) (fun gls -> - errorlabstrm "DiscrEverywhere" (str"No discriminable equalities")) + errorlabstrm "DiscrEverywhere" (str"No discriminable equalities.")) let discr_tac with_evars = function | None -> discrEverywhere with_evars @@ -714,7 +714,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (* the_conv_x had a side-effect on evdref *) dflt else - error "Cannot solve an unification problem" + error "Cannot solve an unification problem." else let (a,p_i_minus_1) = match whd_beta_stack p_i with | (_sigS,[a;p]) -> (a,p) @@ -856,7 +856,7 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns = (pf,ty)) posns in if injectors = [] then - errorlabstrm "Equality.inj" (str "Failed to decompose the equality"); + errorlabstrm "Equality.inj" (str "Failed to decompose the equality."); tclMAP (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf]) injectors @@ -870,10 +870,10 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause = match find_positions env sigma t1 t2 with | Inl _ -> errorlabstrm "Inj" - (str"Not a projectable equality but a discriminable one") + (str"Not a projectable equality but a discriminable one.") | Inr [] -> errorlabstrm "Equality.inj" - (str"Nothing to do, it is an equality between convertible terms") + (str"Nothing to do, it is an equality between convertible terms.") | Inr posns -> (* Est-ce utile ŕ partir du moment oů les arguments projetés subissent "nf" ? let t1 = try_delta_expand env sigma t1 in @@ -977,7 +977,7 @@ let find_elim sort_of_gl lbeq = (match lbeq.rect with | Some eq_rect -> eq_rect | None -> errorlabstrm "find_elim" - (str "this type of substitution is not allowed")) + (str "This type of substitution is not allowed.")) (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *) @@ -1077,11 +1077,10 @@ let try_rewrite tac gls = tac gls with | PatternMatchingFailure -> - errorlabstrm "try_rewrite" (str "Not a primitive equality here") + errorlabstrm "try_rewrite" (str "Not a primitive equality here.") | e when catchable_exception e -> errorlabstrm "try_rewrite" - (str "Cannot find a well-typed generalization of the goal that" ++ - str " makes the proof progress") + (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") let cutSubstClause l2r eqn cls gls = match cls with @@ -1136,7 +1135,7 @@ let unfold_body x gl = match Sign.lookup_named x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis") in + (pr_id x ++ str" is not a defined hypothesis.") in let aft = afterHyp x gl in let hl = List.fold_right (fun (y,yval,_) cl -> ((all_occurrences_expr,y),InHyp) :: cl) aft [] in @@ -1173,7 +1172,8 @@ let subst_one x gl = let test hyp _ = is_eq_x varx hyp in Sign.fold_named_context test ~init:() hyps; errorlabstrm "Subst" - (str "cannot find any non-recursive equality over " ++ pr_id x) + (str "Cannot find any non-recursive equality over " ++ pr_id x ++ + str".") with FoundHyp res -> res in (* The set of hypotheses using x *) @@ -1254,7 +1254,7 @@ let cond_eq_term c t gl = let rewrite_multi_assumption_cond cond_eq_term cl gl = let rec arec = function - | [] -> error "No such assumption" + | [] -> error "No such assumption." | (id,_,t) ::rest -> begin try @@ -1277,7 +1277,7 @@ let replace_multi_term dir_opt c = (* JF. old version let rewrite_assumption_cond faildir gl = let rec arec = function - | [] -> error "No such assumption" + | [] -> error "No such assumption." | (id,_,t)::rest -> (try let dir = faildir t gl in general_rewrite dir (mkVar id) gl @@ -1287,7 +1287,7 @@ let rewrite_assumption_cond faildir gl = let rewrite_assumption_cond_in faildir hyp gl = let rec arec = function - | [] -> error "No such assumption" + | [] -> error "No such assumption." | (id,_,t)::rest -> (try let dir = faildir t gl in general_rewrite_in dir hyp (mkVar id) gl diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index bb279b5ba..8313a0947 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -41,16 +41,16 @@ let instantiate n rawc ido gl = (match decl with (_,None,typ) -> evar_list sigma typ | _ -> error - "please be more specific : in type or value ?") + "Please be more specific: in type or value?") | InHypTypeOnly -> let (_, _, typ) = decl in evar_list sigma typ | InHypValueOnly -> (match decl with (_,Some body,_) -> evar_list sigma body - | _ -> error "not a let .. in hypothesis") in + | _ -> error "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"; + if n <= 0 then error "Incorrect existential variable index."; let ev,_ = destEvar (List.nth evl (n-1)) in let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in tclTHEN diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 302d9a992..4145a8dcc 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -273,7 +273,7 @@ let dest_nf_eq gls eqn = try snd (first_match (match_eq_nf gls eqn) equalities) with PatternMatchingFailure -> - error "Not an equality" + error "Not an equality." (*** Sigma-types *) diff --git a/tactics/inv.ml b/tactics/inv.ml index a25fa285b..6edc723cf 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -101,7 +101,7 @@ let make_inv_predicate env sigma indf realargs id status concl = | Dep dflt_concl -> if not (occur_var env id concl) then errorlabstrm "make_inv_predicate" - (str "Current goal does not depend on " ++ pr_id id); + (str "Current goal does not depend on " ++ pr_id id ++ str"."); (* We abstract the conclusion of goal with respect to realargs and c to * be concl in order to rewrite and have c also rewritten when the case * will be done *) @@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls = let rec tclMAP_i n tacfun = function | [] -> tclDO n (tacfun None) | a::l -> - if n=0 then error "Too much names" + if n=0 then error "Too much names." else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) let remember_first_eq id x = if !x = None then x := Some id @@ -377,22 +377,22 @@ let rewrite_equations_gene othin neqns ba gl = let rec get_names allow_conj = function | IntroWildcard -> - error "Discarding pattern not allowed for inversion equations" + error "Discarding pattern not allowed for inversion equations." | IntroAnonymous -> - error "Anonymous pattern not allowed for inversion equations" + error "Anonymous pattern not allowed for inversion equations." | IntroFresh _-> - error "Fresh pattern not allowed for inversion equations" + error "Fresh pattern not allowed for inversion equations." | IntroRewrite _-> - error "Rewriting pattern not allowed for inversion equations" + error "Rewriting pattern not allowed for inversion equations." | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else let l = List.map (fun id -> Option.get (fst (get_names false id))) l in (Some (List.hd l), l) else - error "Nested conjunctive patterns not allowed for inversion equations" + error"Nested conjunctive patterns not allowed for inversion equations." | IntroOrAndPattern l -> - error "Disjunctive patterns not allowed for inversion equations" + error "Disjunctive patterns not allowed for inversion equations." | IntroIdentifier id -> (Some id,[id]) @@ -453,7 +453,7 @@ let raw_inversion inv_kind id status names gl = try pf_reduce_to_atomic_ind gl (pf_type_of gl c) with UserError _ -> errorlabstrm "raw_inversion" - (str ("The type of "^(string_of_id id)^" is not inductive")) in + (str ("The type of "^(string_of_id id)^" is not inductive.")) in let indclause = mk_clenv_from gl (c,t) in let ccl = clenv_type indclause in check_no_metas indclause ccl; @@ -494,7 +494,7 @@ let not_found_message ids = let dep_prop_prop_message id = errorlabstrm "Inv" (str "Inversion on " ++ pr_id id ++ - str " would needs dependent elimination Prop-Prop") + str " would need dependent elimination from Prop to Prop.") let not_inductive_here id = errorlabstrm "mind_specif_of_mind" diff --git a/tactics/leminv.ml b/tactics/leminv.ml index b43466e31..c1f20e8c3 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -214,7 +214,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = (ids_of_named_context (named_context invEnv))); (* errorlabstrm "lemma_inversion" - (str"Computed inversion goal was not closed in initial signature"); + (str"Computed inversion goal was not closed in initial signature."); *) let invSign = named_context_val invEnv in let pfs = mk_pftreestate (mk_goal invSign invGoal None) in @@ -272,7 +272,7 @@ let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Cannot compute lemma inversion when there are" ++ spc () ++ str"free variables in the types of an inductive" ++ spc () ++ - str"which are not free in its instance"); *) + str"which are not free in its instance."); *) add_inversion_lemma na env sigma t sort dep_option inv_op let add_inversion_lemma_exn na com comsort bool tac = diff --git a/tactics/refine.ml b/tactics/refine.ml index 3dc829462..39567f981 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -229,7 +229,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with (* Produit. Est-ce bien exact ? *) | Prod (_,_,_) -> if occur_meta c then - error "Refine: proof term contains metas in a product" + error "refine: proof term contains metas in a product." else TH (c,[],[]) @@ -330,7 +330,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | Fix ((ni,_),(fi,ai,_)) , _ -> let out_name = function | Name id -> id - | _ -> error "recursive functions must have names !" + | _ -> error "Recursive functions must have names." in let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in tclTHENS @@ -345,7 +345,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | CoFix (_,(fi,ai,_)) , _ -> let out_name = function | Name id -> id - | _ -> error "recursive functions must have names !" + | _ -> error "Recursive functions must have names." in let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in tclTHENS diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index fc3673e6f..f81f15d89 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -57,7 +57,7 @@ let safe_msgnl s = let error_syntactic_metavariables_not_allowed loc = user_err_loc (loc,"out_ident", - str "Syntactic metavariables allowed only in quotations") + str "Syntactic metavariables allowed only in quotations.") let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid @@ -111,7 +111,7 @@ type interp_sign = let check_is_value = function | VRTactic _ -> (* These are goals produced by Match *) - error "Immediate match producing tactics not allowed in local definitions" + error "Immediate match producing tactics not allowed in local definitions." | _ -> () (* For tactic_of_value *) @@ -121,7 +121,7 @@ exception NotTactic let constr_of_VConstr_context = function | VConstr_context c -> c | _ -> - errorlabstrm "constr_of_VConstr_context" (str "not a context variable") + errorlabstrm "constr_of_VConstr_context" (str "Not a context variable.") (* Displays a value *) let rec pr_value env = function @@ -192,7 +192,7 @@ let find_reference env qid = let error_not_evaluable s = errorlabstrm "evalref_of_ref" (str "Cannot coerce" ++ spc () ++ s ++ spc () ++ - str "to an evaluable reference") + str "to an evaluable reference.") (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty @@ -260,7 +260,7 @@ let tac_tab = Hashtbl.create 17 let add_tactic s t = if Hashtbl.mem tac_tab s then errorlabstrm ("Refiner.add_tactic: ") - (str ("Cannot redeclare tactic "^s)); + (str ("Cannot redeclare tactic "^s^".")); Hashtbl.add tac_tab s t let overwriting_add_tactic s t = @@ -275,7 +275,7 @@ let lookup_tactic s = Hashtbl.find tac_tab s with Not_found -> errorlabstrm "Refiner.lookup_tactic" - (str"The tactic " ++ str s ++ str" is not installed") + (str"The tactic " ++ str s ++ str" is not installed.") (* let vernac_tactic (s,args) = let tacfun = lookup_tactic s args in @@ -312,7 +312,7 @@ let lookup_genarg_subst id = let (_,_,f) = lookup_genarg id in f let coerce_to_tactic loc id = function | VTactic _ | VFun _ | VRTactic _ as a -> a | _ -> user_err_loc - (loc, "", str "variable " ++ pr_id id ++ str " should be bound to a tactic") + (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") (*****************) (* Globalization *) @@ -641,7 +641,7 @@ let extern_tacarg ch env sigma = function | VConstr c -> !print_xml_term ch env sigma c | VTactic _ | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _ | VIntroPattern _ | VRec _ | VList _ -> - error "Only externing of terms is implemented" + error "Only externing of terms is implemented." let extern_request ch req gl la = output_string ch "<REQUEST req=\""; output_string ch req; @@ -679,7 +679,7 @@ let extract_let_names lrc = (fun ((loc,name),_) l -> if List.mem name l then user_err_loc - (loc, "glob_tactic", str "This variable is bound several times"); + (loc, "glob_tactic", str "This variable is bound several times."); name::l) lrc [] @@ -1019,8 +1019,8 @@ let read_pattern lfun = function let cons_and_check_name id l = if List.mem id l then user_err_loc (dloc,"read_match_context_hyps", - str ("Hypothesis pattern-matching variable "^(string_of_id id)^ - " used twice in the same pattern")) + strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^ + " used twice in the same pattern.")) else id::l let rec read_match_context_hyps lfun lidh = function @@ -1160,8 +1160,8 @@ let debugging_exception_step ist signal_anomaly e pp = let error_ltac_variable loc id env v s = user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ - str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ - strbrk "which cannot be coerced to " ++ str s) + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + strbrk "which cannot be coerced to " ++ str s ++ str".") exception CannotCoerceTo of string @@ -1221,8 +1221,9 @@ let coerce_to_int = function let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid - with Not_found -> user_err_loc(fst locid,"interp_int", - str "Unbound variable" ++ pr_id (snd locid)) + with Not_found -> + user_err_loc(fst locid,"interp_int", + str "Unbound variable" ++ pr_id (snd locid) ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid @@ -1259,7 +1260,7 @@ let interp_hyp ist gl (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found") + else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.") let hyp_list_of_VList env = function | VList l -> List.map (coerce_to_hyp env) l @@ -1277,7 +1278,7 @@ let interp_clause_pattern ist gl (l,occl) = | (hyp,l) :: rest -> let hyp = interp_hyp ist gl hyp in if List.mem hyp acc then - error ("Hypothesis "^(string_of_id hyp)^" occurs twice"); + error ("Hypothesis "^(string_of_id hyp)^" occurs twice."); (hyp,l)::(check (hyp::acc) rest) | [] -> [] in (l,check [] occl) @@ -1582,7 +1583,7 @@ let interp_may_eval f ist gl = function with | Not_found -> user_err_loc (loc, "interp_may_eval", - str "Unbound context identifier" ++ pr_id s)) + str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> pf_type_of gl (f ist gl c) | ConstrTerm c -> try @@ -1627,7 +1628,7 @@ let rec interp_message ist = function | MsgIdent (loc,id) :: l -> let v = try List.assoc id ist.lfun - with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found") in + with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in pr_arg message_of_value v ++ interp_message ist l let rec interp_message_nl ist = function @@ -1832,14 +1833,14 @@ and interp_app ist gl fv largs loc = VFun(newlfun@olfun,lvar,body) | _ -> user_err_loc (loc, "Tacinterp.interp_app", - (str"Illegal tactic application")) + (str"Illegal tactic application.")) (* Gives the tactic corresponding to the tactic value *) and tactic_of_value vle g = match vle with | VRTactic res -> res | VTactic (loc,tac) -> catch_error loc tac g - | VFun _ -> error "A fully applied tactic is expected" + | VFun _ -> error "A fully applied tactic is expected." | _ -> raise NotTactic (* Evaluation with FailError catching *) @@ -1919,7 +1920,7 @@ and interp_match_context ist goal lz lr lmr = (v 0 (str "No matching clauses for match goal" ++ (if ist.debug=DebugOff then fnl() ++ str "(use \"Set Ltac Debug\" for more info)" - else mt()))) + else mt()) ++ str".")) end in apply_match_context ist env goal 0 lmr (read_match_rule (fst (constr_list ist env)) lmr) @@ -2081,7 +2082,7 @@ and interp_match ist g lz constr lmr = with PatternMatchingFailure -> apply_match ist csr tl) | _ -> errorlabstrm "Tacinterp.apply_match" (str - "No matching clauses for match") in + "No matching clauses for match.") in let csr = try interp_ltac_constr ist g constr with e -> debugging_exception_step ist true e @@ -2139,13 +2140,13 @@ and interp_ltac_constr ist gl e = | VIntroPattern _ -> str "VIntroPattern" | VConstr_context _ -> str "VConstrr_context" | VRec _ -> str "VRec" - | VList _ -> str "VList")) + | VList _ -> str "VList") ++ str".") (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac gl = try tactic_of_value (val_interp ist gl tac) gl with NotTactic -> - errorlabstrm "" (str "Must be a command or must give a tactic value") + errorlabstrm "" (str "Must be a command or must give a tactic value.") (* Interprets a primitive tactic *) and interp_atomic ist gl = function @@ -2359,14 +2360,14 @@ and interp_atomic ist gl = function | ExtraArgType _ | BindingsArgType | OptArgType _ | PairArgType _ | List0ArgType _ | List1ArgType _ - -> error "This generic type is not supported in alias" + -> error "This generic type is not supported in alias." in let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body) in try tactic_of_value v gl - with NotTactic -> user_err_loc (loc,"",str "not a tactic") + with NotTactic -> user_err_loc (loc,"",str "Not a tactic.") let make_empty_glob_sign () = { ltacvars = ([],[]); ltacrecvars = []; @@ -2773,7 +2774,7 @@ let print_ltac id = with Not_found -> errorlabstrm "print_ltac" - (pr_qualid id ++ spc() ++ str "is not a user defined tactic") + (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") open Libnames @@ -2790,14 +2791,14 @@ let make_absolute_name ident repl = if repl then id, kn else user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is already an Ltac named " ++ pr_reference ident) + str "There is already an Ltac named " ++ pr_reference ident ++ str".") else if is_atomic_kn kn then user_err_loc (loc,"Tacinterp.add_tacdef", - str "Reserved Ltac name " ++ pr_reference ident) + str "Reserved Ltac name " ++ pr_reference ident ++ str".") else id, kn with Not_found -> user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is no Ltac named " ++ pr_reference ident) + str "There is no Ltac named " ++ pr_reference ident ++ str".") let rec filter_map f l = let rec aux acc = function diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 3d5fd753e..13ce33444 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -86,7 +86,7 @@ let tclMAP tacfun l = let tclNTH_HYP m (tac : constr->tactic) gl = tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) - with Failure _ -> error "No such assumption") gl + with Failure _ -> error "No such assumption.") gl (* apply a tactic to the last element of the signature *) @@ -94,11 +94,11 @@ let tclLAST_HYP = tclNTH_HYP 1 let tclLAST_NHYPS n tac gl = tac (try list_firstn n (pf_ids_of_hyps gl) - with Failure _ -> error "No such assumptions") gl + with Failure _ -> error "No such assumptions.") gl let tclTRY_sign (tac : constr->tactic) sign gl = let rec arec = function - | [] -> tclFAIL 0 (str "no applicable hypothesis") + | [] -> tclFAIL 0 (str "No applicable hypothesis.") | [s] -> tac (mkVar s) (*added in order to get useful error messages *) | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) in @@ -218,7 +218,7 @@ let lastHyp gl = List.hd (pf_ids_of_hyps gl) let nLastHyps n gl = try list_firstn n (pf_hyps gl) - with Failure "firstn" -> error "Not enough hypotheses in the goal" + with Failure "firstn" -> error "Not enough hypotheses in the goal." let onClause t cls gl = t cls gl @@ -282,7 +282,7 @@ let compute_induction_names n = function | IntroOrAndPattern names when List.length names = n -> Array.of_list names | _ -> - errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names") + errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names.") let compute_construtor_signatures isrec (_,k as ity) = let rec analrec c recargs = @@ -335,7 +335,7 @@ let general_elim_then_using mk_elim let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> error "elimination" + | _ -> anomaly "elimination" in let pmv = let p, _ = decompose_app elimclause.templtyp.Evd.rebus in @@ -348,7 +348,7 @@ let general_elim_then_using mk_elim | Var id -> string_of_id id | _ -> "\b" in - error ("The elimination combinator " ^ name_elim ^ " is not known") + error ("The elimination combinator " ^ name_elim ^ " is unknown.") in let elimclause' = clenv_fchain indmv elimclause indclause' in let elimclause' = clenv_match_args elimbindings elimclause' in @@ -423,7 +423,7 @@ let make_elim_branch_assumptions ba gl = id::constargs, recargs, indargs) tl idtl - | (_, _) -> error "make_elim_branch_assumptions" + | (_, _) -> anomaly "make_elim_branch_assumptions" in makerec ([],[],[],[],[]) ba.branchsign (try list_firstn ba.nassums (pf_hyps gl) @@ -447,7 +447,7 @@ let make_case_branch_assumptions ba gl = id::cargs, recargs, id::constargs) tl idtl - | (_, _) -> error "make_case_branch_assumptions" + | (_, _) -> anomaly "make_case_branch_assumptions" in makerec ([],[],[],[]) ba.branchsign (try list_firstn ba.nassums (pf_hyps gl) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c8f92b60f..1fdd4c16f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -98,7 +98,7 @@ let string_of_inductive c = let (mib,mip) = Global.lookup_inductive ind_sp in string_of_id mip.mind_typename | _ -> raise Bound - with Bound -> error "Bound head variable" + with Bound -> error "Bound head variable." let rec head_constr_bound t l = let t = strip_outer_cast(collapse_appl t) in @@ -114,7 +114,7 @@ let rec head_constr_bound t l = | _ -> raise Bound let head_constr c = - try head_constr_bound c [] with Bound -> error "Bound head variable" + try head_constr_bound c [] with Bound -> error "Bound head variable." (* let bad_tactic_args s l = @@ -174,7 +174,7 @@ let reduct_in_hyp redfun ((_,id),where) gl = match c with | None -> if where = InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value"); + errorlabstrm "" (pr_id id ++ str "has no value."); convert_hyp_no_check (id,None,redfun' ty) gl | Some b -> let b' = if where <> InHypTypeOnly then redfun' b else b in @@ -197,7 +197,7 @@ let change_and_check cv_pb t env sigma c = if is_fconv cv_pb env sigma t c then t else - errorlabstrm "convert-check-hyp" (str "Not convertible") + errorlabstrm "convert-check-hyp" (str "Not convertible.") (* Use cumulutavity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb t = function @@ -219,7 +219,7 @@ let change occl c cls = ({onhyps=(Some(_::_::_)|None)} |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}), Some _ -> - error "No occurrences expected when changing several hypotheses" + error "No occurrences expected when changing several hypotheses." | _ -> ()); onClauses (change_option occl c) cls @@ -300,7 +300,7 @@ let find_name decl gl = function | IntroBasedOn (id,idl) -> fresh_id idl id gl | IntroMustBe id -> let id' = fresh_id [] id gl in - if id' <> id then error ((string_of_id id)^" is already used"); + if id' <> id then error ((string_of_id id)^" is already used."); id' (* Returns the names that would be created by intros, without doing @@ -337,7 +337,7 @@ let rec intro_gen name_flag move_flag force_flag gl = (reduce (Red true) onConcl) (intro_gen name_flag move_flag force_flag) gl with Redelimination -> - errorlabstrm "Intro" (str "No product even after head-reduction") + errorlabstrm "Intro" (str "No product even after head-reduction.") let intro_mustbe_force id = intro_gen (IntroMustBe id) None true let intro_using id = intro_gen (IntroBasedOn (id,[])) None false @@ -415,7 +415,8 @@ let depth_of_quantified_hypothesis red h gl = errorlabstrm "lookup_quantified_hypothesis" (str "No " ++ msg_quantified_hypothesis h ++ strbrk " in current goal" ++ - if red then strbrk " even after head-reduction" else mt ()) + (if red then strbrk " even after head-reduction" else mt ()) ++ + str".") let intros_until_gen red h g = tclDO (depth_of_quantified_hypothesis red h g) intro g @@ -515,7 +516,7 @@ let cut c gl = (internal_cut_rev id c) (tclTHEN (apply_type t [mkVar id]) (thin [id])) gl - | _ -> error "Not a proposition or a type" + | _ -> error "Not a proposition or a type." let cut_intro t = tclTHENFIRST (cut t) intro @@ -543,7 +544,7 @@ let cut_in_parallel l = let error_uninstantiated_metas t clenv = let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta" - in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id) + in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") let clenv_refine_in with_evars id clenv gl = let clenv = clenv_pose_dependent_evars with_evars clenv in @@ -577,7 +578,7 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl = (match kind_of_term (last_arg elimclause.templval.rebus) with | Meta mv -> mv | _ -> errorlabstrm "elimination_clause" - (str "The type of elimination clause is not well-formed")) + (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain indmv elimclause indclause in res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags @@ -648,7 +649,7 @@ let elimination_in_clause_scheme with_evars id elimclause indclause gl = match clenv_independent elimclause with [k1;k2] -> (k1,k2) | _ -> errorlabstrm "elimination_clause" - (str "The type of elimination clause is not well-formed") in + (str "The type of elimination clause is not well-formed.") in let elimclause' = clenv_fchain indmv elimclause indclause in let hyp = mkVar id in let hyp_typ = pf_type_of gl hyp in @@ -658,7 +659,7 @@ let elimination_in_clause_scheme with_evars id elimclause indclause gl = let new_hyp_typ = clenv_type elimclause'' in if eq_constr hyp_typ new_hyp_typ then errorlabstrm "general_rewrite_in" - (str "Nothing to rewrite in " ++ pr_id id); + (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id elimclause'' gl let general_elim_in with_evars id = @@ -701,7 +702,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl = let thm_ty0 = nf_betaiota (pf_type_of gl c) in let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in - if n<0 then error "Apply: theorem has not enough premisses."; + if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in try try_apply thm_ty0 concl_nprod @@ -788,10 +789,10 @@ let find_matching_clause unifier clause = let progress_with_clause innerclause clause = let ordered_metas = List.rev (clenv_independent clause) in - if ordered_metas = [] then error "Statement without assumptions"; + if ordered_metas = [] then error "Statement without assumptions."; let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in try list_try_find f ordered_metas - with Failure _ -> error "Unable to unify" + with Failure _ -> error "Unable to unify." let apply_in_once gl innerclause (d,lbind) = let thm = nf_betaiota (pf_type_of gl d) in @@ -832,7 +833,7 @@ let cut_and_apply c gl = tclTHENLAST (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())]) (apply_term c [mkMeta (new_meta())]) gl - | _ -> error "Imp_elim needs a non-dependent product" + | _ -> error "lapply needs a non-dependent product." (********************************************************************) (* Exact tactics *) @@ -844,7 +845,7 @@ let exact_check c gl = if pf_conv_x_leq gl ct concl then refine_no_check c gl else - error "Not an exact proof" + error "Not an exact proof." let exact_no_check = refine_no_check @@ -863,7 +864,7 @@ let (assumption : tactic) = fun gl -> let hyps = pf_hyps gl in let rec arec only_eq = function | [] -> - if only_eq then arec false hyps else error "No such assumption" + if only_eq then arec false hyps else error "No such assumption." | (id,c,t)::rest -> if (only_eq & eq_constr t concl) or (not only_eq & pf_conv_x_leq gl t concl) @@ -919,7 +920,8 @@ let specialize mopt (c,lbind) g = let term = applist(thd,tstack) in if occur_meta term then errorlabstrm "" (str "Cannot infer an instance for " ++ - pr_name (meta_name clause.evd (List.hd (collect_metas term)))); + pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ + str "."); Some (evars_of clause.evd), term in tclTHEN @@ -955,14 +957,14 @@ let keep hyps gl = (************************) let check_number_of_constructors expctdnumopt i nconstr = - if i=0 then error "The constructors are numbered starting from 1"; + if i=0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when n <> nconstr -> error ("Not an inductive goal with "^ - string_of_int n^plural n " constructor") + string_of_int n^plural n " constructor"^".") | _ -> () end; - if i > nconstr then error "Not enough constructors" + if i > nconstr then error "Not enough constructors." let constructor_tac with_evars expctdnumopt i lbind gl = let cl = pf_concl gl in @@ -987,7 +989,7 @@ let any_constructor with_evars tacopt gl = let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in let nconstr = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in - if nconstr = 0 then error "The type has no constructors"; + if nconstr = 0 then error "The type has no constructors."; tclFIRST (List.map (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t) @@ -1033,11 +1035,11 @@ let intro_or_and_pattern ll l' tac = | [] when n = 0 or tail -> [] | [] -> IntroAnonymous :: adjust_names_length tail (n-1) [] | _ :: _ as l when n = 0 -> - if tail then l else error "Too many names in some branch" + if tail then l else error "Too many names in some branch." | ip :: l -> ip :: adjust_names_length tail (n-1) l in let ll = fix_empty_case nv ll in if List.length ll <> Array.length nv then - error "Not the right number of patterns"; + error "Not the right number of patterns."; tclTHENLASTn (tclTHEN case_last clear_last) (array_map2 (fun n l -> tac ((adjust_names_length (l'=[]) n l)@l')) @@ -1140,7 +1142,7 @@ let assert_as first ipat c gl = let id,tac = prepare_intros s ipat gl in tclTHENS ((if first then internal_cut else internal_cut_rev) id c) (if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl - | _ -> error "Not a proposition or a type" + | _ -> error "Not a proposition or a type." let assert_tac first na = assert_as first (ipat_of_name na) let true_cut = assert_tac true @@ -1349,7 +1351,7 @@ let letin_tac with_eq name c occs gl = let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in if name = Anonymous then fresh_id [] x gl else if not (mem_named_context x (pf_hyps gl)) then x else - error ("The variable "^(string_of_id x)^" is already declared") in + error ("The variable "^(string_of_id x)^" is already declared.") in let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in let t = pf_type_of gl c in let newcl,eq_tac = match with_eq with @@ -1390,7 +1392,7 @@ let unfold_body x gl = match Sign.lookup_named x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis") in + (pr_id x ++ str" is not a defined hypothesis.") in let aft = afterHyp x gl in let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in let xvar = mkVar x in @@ -1764,7 +1766,7 @@ let empty_scheme = hypothesis on which the induction is made *) let induction_tac with_evars (varname,lbind) typ scheme gl = let elimc,lbindelimc = - match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in + match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in let elimt = scheme.elimt in let indclause = make_clenv_binding gl (mkVar varname,typ) lbind in let elimclause = @@ -1825,7 +1827,7 @@ let chop_context n l = let error_ind_scheme s = let s = if s <> "" then s^" " else s in - error ("Cannot recognise "^s^"an induction schema") + error ("Cannot recognize "^s^"an induction scheme.") let mkEq t x y = mkApp (build_coq_eq (), [| t; x; y |]) @@ -2033,13 +2035,13 @@ let decompose_paramspred_branch_args elimt = then cut_noccur elimt' ((nme,None,tpe)::acc2) else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl | App(_, _) | Rel _ -> acc2 , [] , elimt - | _ -> error "cannot recognise an induction schema" in + | _ -> error_ind_scheme "" in let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types = match kind_of_term elimt with | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1) | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl | App(_, _) | Rel _ -> acc1,[],[],elimt - | _ -> error "cannot recognise an induction schema" in + | _ -> error_ind_scheme "" in let acc1, acc2 , acc3, ccl = cut_occur elimt [] in (* Particular treatment when dealing with a dependent empty type elim scheme: if there is no branch, then acc1 contains all hyps which is wrong (acc1 @@ -2053,8 +2055,7 @@ let decompose_paramspred_branch_args elimt = let hd_ccl_pred,_ = decompose_app ccl in match kind_of_term hd_ccl_pred with | Rel i -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl - | _ -> error "cannot recognize an induction schema" - + | _ -> error_ind_scheme "" let exchange_hd_app subst_hd t = @@ -2131,7 +2132,7 @@ let compute_elim_sig ?elimc elimt = (* 3- Look at last arg: is it the indarg? *) ignore ( match List.hd args_indargs with - | hiname,Some _,hi -> error "cannot recognize an induction schema" + | hiname,Some _,hi -> error_ind_scheme "" | hiname,None,hi -> let hi_ind, hi_args = decompose_app hi in let hi_is_ind = (* hi est d'un type globalisable *) @@ -2156,11 +2157,11 @@ let compute_elim_sig ?elimc elimt = with Exit -> (* Ending by computing indrev: *) match !res.indarg with | None -> !res (* No indref *) - | Some ( _,Some _,_) -> error "Cannot recognise an induction scheme" + | Some ( _,Some _,_) -> error_ind_scheme "" | Some ( _,None,ind) -> let indhd,indargs = decompose_app ind in try {!res with indref = Some (global_of_constr indhd) } - with _ -> error "Cannot find the inductive type of the inductive schema";; + with _ -> error "Cannot find the inductive type of the inductive scheme.";; (* Check that the elimination scheme has a form similar to the elimination schemes built by Coq. Schemes may have the standard @@ -2174,7 +2175,7 @@ let compute_elim_signature elimc elimt names_info = let f,l = decompose_app scheme.concl in (* Vérifier que les arguments de Qi sont bien les xi. *) match scheme.indarg with - | Some (_,Some _,_) -> error "strange letin, cannot recognize an induction schema" + | Some (_,Some _,_) -> error "Strange letin, cannot recognize an induction scheme." | None -> (* Non standard scheme *) let npred = List.length scheme.predicates in let is_pred n c = @@ -2242,7 +2243,7 @@ let compute_elim_signature elimc elimt names_info = list_lastn scheme.nargs indargs = extended_rel_list 0 scheme.args in if not (ccl_arg_ok & ind_is_ok) then - error "Cannot recognize the conclusion of an induction schema"; + error_ind_scheme "the conclusion of"; [] in let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in @@ -2285,7 +2286,7 @@ let recolle_clenv scheme lid elimclause gl = match kind_of_term x with | Meta mv -> mv | _ -> errorlabstrm "elimination_clause" - (str "The type of elimination clause is not well-formed")) + (str "The type of the elimination clause is not well-formed.")) arr in let nmv = Array.length lindmv in let lidparams,lidargs = cut_list (scheme.nparams) lid in @@ -2324,7 +2325,7 @@ let recolle_clenv scheme lid elimclause gl = let induction_tac_felim with_evars indvars (* (elimc,lbindelimc) elimt *) scheme gl = let elimt = scheme.elimt in let elimc,lbindelimc = - match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in + match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) let elimclause = make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in @@ -2348,7 +2349,7 @@ let induction_from_context_l isrec with_evars elim_info lid names gl = + (if scheme.indarg <> None then 1 else 0) in (* Number of given induction args must be exact. *) if List.length lid <> nargs_indarg_farg + scheme.nparams then - error "not the right number of arguments given to induction scheme"; + error "Not the right number of arguments given to induction scheme."; let env = pf_env gl in (* hyp0 is used for re-introducing hyps at the right place afterward. We chose the first element of the list of variables on which to @@ -2466,7 +2467,7 @@ let induction_without_atomization isrec with_evars elim names lid gl = in let nlid = List.length lid in if nlid <> awaited_nargs - then error "Not the right number of induction arguments" + then error "Not the right number of induction arguments." else induction_from_context_l isrec with_evars elim_info lid names gl let new_induct_gen isrec with_evars elim names (c,lbind) cls gl = @@ -2532,18 +2533,18 @@ let induct_destruct_l isrec with_evars lc elim names cls = let _ = if elim = None then - error ("Induction scheme must be given when several induction hypothesis.\n" - ^ "Example: induction x1 x2 x3 using my_scheme.") in + errorlabstrm "" (strbrk "Induction scheme must be given when several induction hypothesis are given.\n" ++ + str "Example: induction x1 x2 x3 using my_scheme.") in let newlc = List.map (fun x -> match x with (* FIXME: should we deal with ElimOnIdent? *) | ElimOnConstr (x,NoBindings) -> x - | _ -> error "don't know where to find some argument") + | _ -> error "Don't know where to find some argument.") lc in if cls <> None then error - "'in' clause not supported when several induction hypothesis are given"; + "'in' clause not supported when several induction hypothesis are given."; new_induct_gen_l isrec with_evars elim names newlc (* Induction either over a term, over a quantified premisse, or over @@ -2858,7 +2859,7 @@ let abstract_subproof name tac gl = let na = next_global_ident_away false name (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then - error "\"abstract\" cannot handle existentials"; + error "\"abstract\" cannot handle existentials."; let lemme = start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ()); let _,(const,kind,_) = @@ -2901,7 +2902,7 @@ let admit_as_an_axiom gl = let name = add_suffix (get_current_proof_name ()) "_admitted" in let na = next_global_ident_away false name (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in - if occur_existential concl then error "\"admit\" cannot handle existentials"; + if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = let cd = Entries.ParameterEntry (concl,false) in let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 0207f1fb9..4af760ed8 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -165,7 +165,7 @@ let tauto g = try intuition_gen (interp <:tactic<fail>>) g with Refiner.FailError _ | UserError _ -> - errorlabstrm "tauto" [< str "tauto failed" >] + errorlabstrm "tauto" (str "tauto failed.") let default_intuition_tac = interp <:tactic< auto with * >> diff --git a/test-suite/bugs/opened/shouldnotfail/1671.v b/test-suite/bugs/opened/shouldnotfail/1671.v new file mode 100644 index 000000000..800c431ec --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1671.v @@ -0,0 +1,12 @@ +(* Exemple soumis par Pierre Corbineau (bug #1671) *) + +CoInductive hdlist : unit -> Type := +| cons : hdlist tt -> hdlist tt. + +Variable P : forall bo, hdlist bo -> Prop. +Variable all : forall bo l, P bo l. + +Definition F (l:hdlist tt) : P tt l := +match l in hdlist u return P u l with +| cons (cons l') => all tt _ +end. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 149901c7b..a4eb8bbcc 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) (* Extract Inductive sigT => "prod" [ "" ]. *) -*) +*)
\ No newline at end of file diff --git a/toplevel/class.ml b/toplevel/class.ml index 5e0713ea9..7ad7c0eda 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -119,7 +119,7 @@ let class_of_global = function | ConstructRef _ as c -> errorlabstrm "class_of_global" (str "Constructors, such as " ++ Printer.pr_global c ++ - str " cannot be used as class") + str ", cannot be used as a class.") (* lp est la liste (inverse'e) des arguments de la coercion @@ -189,7 +189,7 @@ let ident_key_of_class = function let error_not_transparent source = errorlabstrm "build_id_coercion" - (pr_class source ++ str " must be a transparent constant") + (pr_class source ++ str " must be a transparent constant.") let build_id_coercion idf_opt source = let env = Global.env () in @@ -218,8 +218,8 @@ let build_id_coercion idf_opt source = (Reductionops.is_conv_leq env Evd.empty (Typing.type_of env Evd.empty val_f) typ_f) then - error ("cannot be defined as coercion - "^ - "maybe a bad number of arguments") + errorlabstrm "" (strbrk + "Cannot be defined as coercion (maybe a bad number of arguments).") in let idf = match idf_opt with @@ -283,7 +283,8 @@ let add_new_coercion_core coef stre source target isid = let try_add_new_coercion_core ref b c d e = try add_new_coercion_core ref b c d e with CoercionError e -> - errorlabstrm "try_add_new_coercion_core" (explain_coercion_error ref e) + errorlabstrm "try_add_new_coercion_core" + (explain_coercion_error ref e ++ str ".") let try_add_new_coercion ref stre = try_add_new_coercion_core ref stre None None false diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 1837bca9a..e4df5acbf 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -50,14 +50,14 @@ let declare_instance_cst glob con = let _, r = decompose_prod_assum instance in match class_of_constr r with | Some tc -> add_instance (new_instance tc None glob con) - | None -> error "Constant does not build instances of a declared type class" + | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") let declare_instance glob idl = let con = try (match global (Ident idl) with | ConstRef x -> x | _ -> raise Not_found) - with _ -> error "Instance definition not found" + with _ -> error "Instance definition not found." in declare_instance_cst glob con let mismatched_params env n m = mismatched_ctx_inst env Parameters n m @@ -385,7 +385,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau Name id -> let sp = Lib.make_path id in if Nametab.exists_cci sp then - errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); + errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists."); id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in @@ -480,7 +480,7 @@ let context ?(hook=fun _ -> ()) l = let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; let ctx = try named_of_rel_context fullctx with _ -> - error "Anonymous variables not allowed in contexts" + error "Anonymous variables not allowed in contexts." in List.iter (function (id,_,t) -> if Lib.is_modtype () then diff --git a/toplevel/command.ml b/toplevel/command.ml index c3bddf1d9..d245dcbc1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -88,8 +88,8 @@ let rec complete_conclusion a cs = function let (has_no_args,name,params) = a in if not has_no_args then user_err_loc (loc,"", - str "Cannot infer the non constant arguments of the conclusion of " - ++ pr_id cs); + strbrk"Cannot infer the non constant arguments of the conclusion of " + ++ pr_id cs ++ str "."); let args = List.map (fun id -> CRef(Ident(loc,id))) params in CAppExpl (loc,(None,Ident(loc,name)),List.rev args) | c -> c @@ -310,7 +310,7 @@ let declare_eq_scheme sp = definition_message nam done with Not_found -> - error "Your type contains Parameters without a boolean equality" + error "Your type contains Parameters without a boolean equality." (* decidability of eq *) @@ -473,7 +473,7 @@ type inductive_expr = { } let minductive_message = function - | [] -> error "no inductive definition" + | [] -> error "No inductive definition." | [x] -> (pr_id x ++ str " is defined") | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ spc () ++ str "are defined") @@ -597,7 +597,7 @@ let extract_params indl = | [] -> anomaly "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"; + "Parameters should be syntactically the same for each inductive type."; params let prepare_inductive ntnl indl = @@ -672,7 +672,7 @@ let recursive_message indexes = function | None -> mt ()) let corecursive_message _ = function - | [] -> error "no corecursive definition" + | [] -> error "No corecursive definition." | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ spc () ++ str "are corecursively defined") @@ -1005,7 +1005,7 @@ let build_combined_scheme name schemes = let qualid = qualid_of_reference refe in let cst = try Nametab.locate_constant (snd qualid) - with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared") + with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.") in let ty = Typeops.type_of_constant env cst in qualid, cst, ty) @@ -1055,7 +1055,7 @@ let compute_proof_name = function | Some (loc,id) -> (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"",pr_id id ++ str " already exists"); + user_err_loc (loc,"",pr_id id ++ str " already exists."); id | None -> next_global_ident_away false (id_of_string "Unnamed_thm") @@ -1207,7 +1207,7 @@ let start_proof_com kind thms hook = let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then - error "This command can only be used for unnamed theorem" + error "This command can only be used for unnamed theorem." (* message("Overriding name "^(string_of_id id)^" and using "^save_ident) *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 53e7ea596..50d30cda7 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -127,7 +127,7 @@ let print_grammar = function Gram.Entry.print Pcoq.Vernac_.gallina; msgnl (str "Entry gallina_ext is"); Gram.Entry.print Pcoq.Vernac_.gallina_ext; - | _ -> error "Unknown or unprintable grammar entry" + | _ -> error "Unknown or unprintable grammar entry." (**********************************************************************) (* Parse a format (every terminal starting with a letter or a single @@ -143,11 +143,11 @@ let parse_format (loc,str) = if 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 + | _ -> error "Non terminated box in format." in let close_quotation i = if i < String.length str & str.[i] = '\'' & (i+1 = l or str.[i+1] = ' ') then i+1 - else error "Incorrectly terminated quoted expression" in + else error "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 @@ -155,10 +155,10 @@ let parse_format (loc,str) = if i < String.length str & str.[i] <> ' ' then if str.[i] = '\'' & quoted & (i+1 >= String.length str or str.[i+1] = ' ') - then if n=0 then error "Empty quoted token" else n + then if n=0 then error "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 error "Spaces are not allowed in (quoted) symbols." else n in let rec parse_non_format i = let n = nonspaces false 0 i in @@ -189,8 +189,8 @@ let parse_format (loc,str) = (* 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" + | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format." + else error "\"v\", \"hv\" or \" \" expected after \"[\" in format." (* Parse "]" *) | ']' -> ([] :: parse_token (close_quotation (i+1))) @@ -201,7 +201,7 @@ let parse_format (loc,str) = (parse_token (close_quotation (i+n)))) else if n = 0 then [] - else error "Ending spaces non part of a format annotation" + else error "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))) @@ -223,9 +223,9 @@ let parse_format (loc,str) = try if str <> "" then match parse_token 0 with | [l] -> l - | _ -> error "Box closed without being opened in format" + | _ -> error "Box closed without being opened in format." else - error "Empty format" + error "Empty format." with e -> Stdpp.raise_with_loc loc e @@ -274,11 +274,11 @@ let rec find_pattern xl = function | [NonTerminal x], NonTerminal x' :: l' -> (x,x',xl),l' | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ -> - error ("The token "^s^" occurs on one side of \"..\" but not on the other side") + error ("The token "^s^" occurs on one side of \"..\" but not on the other side.") | [NonTerminal _], Break s :: _ | Break s :: _, _ -> - error ("A break occurs on one side of \"..\" but not on the other side") + error ("A break occurs on one side of \"..\" but not on the other side.") | ((SProdList _ | NonTerminal _) :: _ | []), _ -> - error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\"") + error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") let rec interp_list_parser hd = function | [] -> [], List.rev hd @@ -320,12 +320,13 @@ let rec raw_analyse_notation_tokens = function | String ".." :: sl -> let (vars,l) = raw_analyse_notation_tokens sl in (list_add_set ldots_var vars, NonTerminal ldots_var :: l) + | String "_" :: _ -> error "_ must be quoted." | String x :: sl when is_normal_token x -> Lexer.check_ident x; let id = Names.id_of_string x in let (vars,l) = raw_analyse_notation_tokens sl in if List.mem id vars then - error ("Variable "^x^" occurs more than once"); + error ("Variable "^x^" occurs more than once."); (id::vars, NonTerminal id :: l) | String s :: sl -> Lexer.check_keyword s; @@ -481,7 +482,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 () = error "The format does not match the notation." let rec split_format_at_ldots hd = function | UnpTerminal s :: fmt when id_of_string s = ldots_var -> List.rev hd, fmt @@ -494,7 +495,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") + error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.") with Exit -> ()) | _ -> () @@ -512,7 +513,7 @@ let read_recursive_format sl fmt = let rec get_tail = function | a :: sepfmt, b :: fmt when a = b -> get_tail (sepfmt, fmt) | [], 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 + | _ -> error "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) @@ -594,7 +595,7 @@ let make_production etyps symbols = let y = match List.assoc x etyps with | ETConstr x -> x | _ -> - error "Component of recursive patterns in notation must be constr" in + error "Component of recursive patterns in notation must be constr." in let typ = ETConstrList (y,sl) in NonTerm (typ, Some (x,typ)) :: l) symbols [] in @@ -640,7 +641,7 @@ let error_incompatible_level ntn oldprec prec = (str ("Notation "^ntn^" is already defined") ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ - pr_level ntn prec) + pr_level ntn prec ++ str ".") let cache_one_syntax_extension (prec,ntn,gr,pp) = try @@ -692,34 +693,34 @@ let interp_modifiers modl = | SetEntryType (s,typ) :: l -> let id = id_of_string s in if List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level"); + error (s^" is already assigned to an entry or constr level."); interp assoc level ((id,typ)::etyps) format l | SetItemLevel ([],n) :: l -> interp assoc level etyps format l | SetItemLevel (s::idl,n) :: l -> let id = id_of_string s in if List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level"); + error (s^" is already assigned to an entry or constr level."); let typ = ETConstr (n,()) in interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l) | SetLevel n :: l -> - if level <> None then error "A level is given more than once"; + if level <> None then error "A level is given more than once."; interp assoc (Some n) etyps format l | SetAssoc a :: l -> - if assoc <> None then error "An associativity is given more than once"; + if assoc <> None then error"An associativity is given more than once."; interp (Some a) level etyps format l | SetOnlyParsing :: l -> onlyparsing := true; interp assoc level etyps format l | SetFormat s :: l -> - if format <> None then error "A format is given more than once"; + if format <> None then error "A format is given more than once."; interp assoc level etyps (Some s) l in interp None None [] None modl let check_infix_modifiers modifiers = let (assoc,level,t,b,fmt) = interp_modifiers modifiers in if t <> [] then - error "explicit entry level or type unexpected in infix notation" + error "explicit entry level or type unexpected in infix notation." let no_syntax_modifiers modifiers = modifiers = [] or modifiers = [SetOnlyParsing] @@ -739,9 +740,9 @@ let set_entry_type etyps (x,typ) = let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then - error "A notation must include at least one symbol"; + error "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" + error "A recursive notation must start with at least one symbol." let is_not_printable = function | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true @@ -752,38 +753,38 @@ let find_precedence lev etyps symbols = | NonTerminal x :: _ -> (try match List.assoc x etyps with | ETConstr _ -> - error "The level of the leftmost non-terminal cannot be changed" + error "The level of the leftmost non-terminal cannot be changed." | ETIdent | ETBigint | ETReference -> if lev = None then - Flags.if_verbose msgnl (str "Setting notation at level 0") + Flags.if_verbose msgnl (str "Setting notation at level 0.") else if lev <> Some 0 then - error "A notation starting with an atomic expression must be at level 0"; + error "A notation starting with an atomic expression must be at level 0."; 0 | ETPattern | ETOther _ -> (* Give a default ? *) if lev = None then - error "Need an explicit level" + error "Need an explicit level." else Option.get lev | ETConstrList _ -> assert false (* internally used in grammar only *) with Not_found -> if lev = None then - error "A left-recursive notation must have an explicit level" + error "A left-recursive notation must have an explicit level." else Option.get lev) | Terminal _ ::l when (match list_last symbols with Terminal _ -> true |_ -> false) -> if lev = None then - (Flags.if_verbose msgnl (str "Setting notation at level 0"); 0) + (Flags.if_verbose msgnl (str "Setting notation at level 0."); 0) else Option.get lev | _ -> - if lev = None then error "Cannot determine the level"; + if lev = None then error "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" +specially and require that the notation \"{ _ }\" is already reserved." (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) let remove_curly_brackets l = @@ -970,7 +971,7 @@ let add_syntax_extension local mv = let add_notation_interpretation df names c sc = try add_notation_interpretation_core false df names c sc false with NoSyntaxRule -> - error "Parsing rule for this notation has to be previously declared" + error "Parsing rule for this notation has to be previously declared." (* Main entry point *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index c64807db1..dd741d40a 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -99,8 +99,8 @@ let dir_ml_load s = (try t.load_obj s with | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u - | _ -> errorlabstrm "Mltop.load_object" [< str"Cannot link ml-object "; - str s; str" to Coq code." >]) + | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ + str s ++ str" to Coq code.")) (* TO DO: .cma loading without toplevel *) | WithoutTop -> IFDEF Byte THEN @@ -116,11 +116,11 @@ let dir_ml_load s = (Filename.basename gname) ".cmo"))] [Filename.dirname gname] with | Dynlink.Error a -> - errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >] + errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) ELSE () END | Native -> errorlabstrm "Mltop.no_load_object" - [< str"Loading of ML object file forbidden in a native Coq" >] + (str"Loading of ML object file forbidden in a native Coq.") (* Dynamic interpretation of .ml *) let dir_ml_use s = @@ -148,7 +148,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Library.add_load_path true (dir,coq_dirpath) end else - msg_warning [< str ("Cannot open " ^ dir) >] + msg_warning (str ("Cannot open " ^ dir)) let convert_string d = try Names.id_of_string d @@ -190,7 +190,7 @@ let file_of_name name = if (is_in_path !coq_mlpath_copy fname) then fname else errorlabstrm "Mltop.load_object" - [< str"File not found on loadpath : "; str (bname^".cm[oa]") >] + (str"File not found on loadpath : " ++ str (bname^".cm[oa]")) (* TODO: supprimer ce hack, si possible *) (* Initialisation of ML modules that need the state (ex: tactics like @@ -247,7 +247,7 @@ let unfreeze_ml_modules x = load_object mname fname else errorlabstrm "Mltop.unfreeze_ml_modules" - [< str"Loading of ML object file forbidden in a native Coq" >]; + (str"Loading of ML object file forbidden in a native Coq."); add_loaded_module mname) x @@ -270,11 +270,11 @@ let cache_ml_module_object (_,{mnames=mnames}) = begin try if_verbose - msg [< str"[Loading ML file "; str fname; str" ..." >]; + msg (str"[Loading ML file " ++ str fname ++ str" ..."); load_object mname fname; - if_verbose msgnl [< str"done]" >] + if_verbose msgnl (str"done]") with e -> - if_verbose msgnl [< str"failed]" >]; + if_verbose msgnl (str"failed]"); raise e end; add_loaded_module mname) @@ -293,11 +293,11 @@ let declare_ml_modules l = let print_ml_path () = let l = !coq_mlpath_copy in - ppnl [< str"ML Load Path:"; fnl (); str" "; - hv 0 (prlist_with_sep pr_fnl pr_str l) >] + ppnl (str"ML Load Path:" ++ fnl () ++ str" " ++ + hv 0 (prlist_with_sep pr_fnl pr_str l)) (* Printing of loaded ML modules *) let print_ml_modules () = let l = get_loaded_modules () in - pp [< str"Loaded ML Modules: " ; pr_vertical_list pr_str l >] + pp (str"Loaded ML Modules: " ++ pr_vertical_list pr_str l) diff --git a/toplevel/record.ml b/toplevel/record.ml index 5a9e014d4..b1271f516 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -87,24 +87,25 @@ type record_error = let warning_or_error coe indsp err = let st = match err with | MissingProj (fi,projs) -> - let s,have = if List.length projs > 1 then "s","have" else "","has" in + let s,have = if List.length projs > 1 then "s","were" else "","was" in (str(string_of_id fi) ++ - str" cannot be defined because the projection" ++ str s ++ spc () ++ - prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++ str "n't.") + strbrk" cannot be defined because the projection" ++ str s ++ spc () ++ + prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++ + strbrk " not defined.") | BadTypedProj (fi,ctx,te) -> match te with | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) -> (pr_id fi ++ - str" cannot be defined because it is informative and " ++ + strbrk" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ - str " is not.") + strbrk " is not.") | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) -> (pr_id fi ++ - str" cannot be defined because it is large and " ++ + strbrk" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ - str " is not.") + strbrk " is not.") | _ -> - (pr_id fi ++ str " cannot be defined because it is not typable") + (pr_id fi ++ strbrk " cannot be defined because it is not typable.") in if coe then errorlabstrm "structure" st; Flags.if_verbose ppnl (hov 0 (str"Warning: " ++ st)) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 758f57c06..d761472c9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -175,7 +175,7 @@ let show_match id = ^ " => \n" ^ acc) "end" patterns in msg (str ("match # with\n" ^ cases)) - with Not_found -> error "Unknown inductive type" + with Not_found -> error "Unknown inductive type." (* "Print" commands *) @@ -251,9 +251,10 @@ let msg_notfound_library loc qid = function let dir = fst (repr_qualid qid) in user_err_loc (loc,"locate_library", strbrk "Cannot find a physical path bound to logical path " ++ - pr_dirpath dir ++ fnl ()) + pr_dirpath dir ++ str".") | Library.LibNotFound -> - msgnl (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid)) + msgnl (hov 0 + (strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")) | e -> assert false let print_located_library r = @@ -312,7 +313,7 @@ let vernac_definition (local,_,_ as k) (loc,id as lid) def hook = | ProveBody (bl,t) -> (* local binders, typ *) if Lib.is_modtype () then errorlabstrm "Vernacentries.VernacDefinition" - (str "Proof editing mode not supported in module types") + (str "Proof editing mode not supported in module types.") else let hook _ _ = () in start_proof_and_print (local,DefinitionBody Definition) @@ -334,10 +335,10 @@ let vernac_start_proof kind l lettop hook = if not(refining ()) then if lettop then errorlabstrm "Vernacentries.StartProof" - (str "Let declarations can only be used in proof editing mode"); + (str "Let declarations can only be used in proof editing mode."); if Lib.is_modtype () then errorlabstrm "Vernacentries.StartProof" - (str "Proof editing mode not supported in module types"); + (str "Proof editing mode not supported in module types."); start_proof_and_print (Global, Proof kind) l hook let vernac_end_proof = function @@ -360,7 +361,7 @@ let vernac_exact_proof c = save_named true end else errorlabstrm "Vernacentries.ExactProof" - (str "Command 'Proof ...' can only be used at the beginning of the proof") + (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.") let vernac_assumption kind l nl= let global = fst kind = Global in @@ -406,7 +407,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = (* 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"; + error "Modules and Module Types are not allowed inside sections."; let binders_ast = List.map (fun (export,idl,ty) -> if export <> None then @@ -426,7 +427,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = (* 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"; + error "Modules and Module Types are not allowed inside sections."; match mexpr_ast_o with | None -> check_no_pending_proofs (); @@ -473,7 +474,7 @@ let vernac_end_module export (loc,id) = let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = if Lib.sections_are_opened () then - error "Modules and Module Types are not allowed inside sections"; + error "Modules and Module Types are not allowed inside sections."; match mty_ast_o with | None -> @@ -537,7 +538,7 @@ let vernac_record struc binders sort nameopt cfs = let s = match kind_of_term s with | Sort s -> s | _ -> user_err_loc - (constr_loc sort,"definition_structure", str "Sort expected") in + (constr_loc sort,"definition_structure", str "Sort expected.") in if !Flags.dump then ( Dumpglob.dump_definition (snd struc) false "rec"; List.iter (fun (_, x) -> @@ -614,7 +615,7 @@ let vernac_declare_instance id = (* Solving *) let vernac_solve n tcom b = if not (refining ()) then - error "Unknown command of the non proof-editing mode"; + error "Unknown command of the non proof-editing mode."; Decl_mode.check_not_proof_mode "Unknown proof instruction"; begin if b then @@ -641,7 +642,7 @@ let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = if not (refining ()) then - error "Unknown command of the non proof-editing mode"; + error "Unknown command of the non proof-editing mode."; if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else () (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) @@ -759,7 +760,7 @@ let vernac_reserve idl c = let make_silent_if_not_pcoq b = if !pcoq <> None then - error "Turning on/off silent flag is not supported in Centaur mode" + error "Turning on/off silent flag is not supported in Pcoq mode." else make_silent b let _ = @@ -1084,7 +1085,7 @@ let global_module r = try Nametab.full_name_module qid with Not_found -> user_err_loc (loc, "global_module", - str "Module/section " ++ pr_qualid qid ++ str " not found") + str "Module/section " ++ pr_qualid qid ++ str " not found.") let interp_search_restriction = function | SearchOutside l -> (List.map global_module l, true) @@ -1131,7 +1132,7 @@ let vernac_goal = function start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); print_subgoals () end else - error "repeated Goal not permitted in refining mode" + error "repeated Goal not permitted in refining mode." let vernac_abort = function | None -> @@ -1149,7 +1150,7 @@ let vernac_abort_all () = delete_all_proofs (); message "Current goals aborted" end else - error "No proof-editing in progress" + error "No proof-editing in progress." let vernac_restart () = restart_proof(); print_subgoals () diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 7d99fe721..8520686d6 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -31,7 +31,7 @@ let vinterp_add s f = Hashtbl.add vernac_tab s f with Failure _ -> errorlabstrm "vinterp_add" - (str"Cannot add the vernac command " ++ str s ++ str" twice") + (str"Cannot add the vernac command " ++ str s ++ str" twice.") let overwriting_vinterp_add s f = begin @@ -46,7 +46,7 @@ let vinterp_map s = Hashtbl.find vernac_tab s with Not_found -> errorlabstrm "Vernac Interpreter" - (str"Cannot find vernac command " ++ str s) + (str"Cannot find vernac command " ++ str s ++ str".") let vinterp_init () = Hashtbl.clear vernac_tab diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 41ec89459..82a2a8449 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -80,7 +80,9 @@ let uri_of_dirpath dir = let error_whelp_unknown_reference ref = let qid = Nametab.shortest_qualid_of_global Idset.empty ref in - error ("Definitions of the current session not supported in Whelp: " ^ string_of_qualid qid) + errorlabstrm "" + (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ + strbrk ", are not supported in Whelp.") let uri_of_repr_kn ref (mp,dir,l) = match mp with @@ -104,7 +106,7 @@ let uri_of_ind_pointer l = let uri_of_global ref = match ref with - | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)) + | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)^".") | ConstRef cst -> uri_of_repr_kn ref (repr_con cst); url_string ".con" | IndRef (kn,i) -> @@ -165,7 +167,7 @@ let rec uri_of_constr c = | RCast (_,c, CastConv (_,t)) -> uri_of_constr c; url_string ":"; uri_of_constr t | RRec _ | RIf _ | RLetTuple _ | RCases _ -> - error "Whelp does not support pattern-matching and (co-)fixpoint" + error "Whelp does not support pattern-matching and (co-)fixpoint." | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) -> anomaly "Written w/o parenthesis" | RPatVar _ | RDynamic _ -> |