diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/modops.ml | 34 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 11 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 2 |
5 files changed, 26 insertions, 25 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e9f8f89adf..f70690af63 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 3b64a2c09c..8ff8ddb85e 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 26030b9e94..d903d4b328 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 fbd4901d6e..eef2d675ce 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 2b28a7147d..ccc62b756d 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 |