diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 1 | ||||
| -rw-r--r-- | kernel/closure.ml | 1 | ||||
| -rw-r--r-- | kernel/conv_oracle.ml | 2 | ||||
| -rw-r--r-- | kernel/cooking.ml | 1 | ||||
| -rw-r--r-- | kernel/declarations.ml | 1 | ||||
| -rw-r--r-- | kernel/environ.ml | 1 | ||||
| -rw-r--r-- | kernel/esubst.ml | 1 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 1 | ||||
| -rw-r--r-- | kernel/inductive.ml | 1 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 1 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 1 | ||||
| -rw-r--r-- | kernel/modops.ml | 1 | ||||
| -rw-r--r-- | kernel/modops.mli | 1 | ||||
| -rw-r--r-- | kernel/names.ml | 4 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 1 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 1 | ||||
| -rw-r--r-- | kernel/sign.ml | 1 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 5 | ||||
| -rw-r--r-- | kernel/term.ml | 1 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 1 | ||||
| -rw-r--r-- | kernel/typeops.ml | 1 | ||||
| -rw-r--r-- | kernel/univ.ml | 5 | ||||
| -rw-r--r-- | kernel/vm.ml | 2 |
26 files changed, 35 insertions, 6 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 8da06f4355..86c8f4913a 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -10,6 +10,7 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) +open Errors open Util open Names open Cbytecodes diff --git a/kernel/closure.ml b/kernel/closure.ml index 143d6eb49a..d62ac79bfe 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -19,6 +19,7 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) +open Errors open Util open Pp open Term diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 92109258d7..c195a5496d 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -44,7 +44,7 @@ let set_strategy k l = cst_opacity := if l=default then Cmap.remove c !cst_opacity else Cmap.add c l !cst_opacity - | RelKey _ -> Util.error "set_strategy: RelKey" + | RelKey _ -> Errors.error "set_strategy: RelKey" let get_transp_state () = (Idmap.fold diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 02330339dd..1a405e98ba 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -14,6 +14,7 @@ declarations over global constants and inductive types *) open Pp +open Errors open Util open Names open Term diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1a84b98768..db304e33d7 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -21,6 +21,7 @@ global constants/axioms, mutual inductive definitions and the module system *) +open Errors open Util open Names open Univ diff --git a/kernel/environ.ml b/kernel/environ.ml index 7a41e62c47..c38d4186fb 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -20,6 +20,7 @@ (* This file defines the type of environments on which the type-checker works, together with simple related functions *) +open Errors open Util open Names open Sign diff --git a/kernel/esubst.ml b/kernel/esubst.ml index cbce04d62a..dad5b1420e 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -10,6 +10,7 @@ (* Support for explicit substitutions *) +open Errors open Util (*********************) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 46e866a047..aa5e132c67 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 21f86233ab..b2d9247148 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 314cc0ee0b..777f391837 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -14,6 +14,7 @@ substitution in module constructions *) open Pp +open Errors open Util open Names open Term diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index a384c836ca..e2304f1194 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -12,6 +12,7 @@ (* This module provides the main functions for type-checking module declarations *) +open Errors open Util open Names open Univ diff --git a/kernel/modops.ml b/kernel/modops.ml index 0c2c6bd71a..a422bae666 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -15,6 +15,7 @@ (* This file provides with various operations on modules and module types *) +open Errors open Util open Pp open Names diff --git a/kernel/modops.mli b/kernel/modops.mli index b9c36d5af4..9f8a306fa9 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/names.ml b/kernel/names.ml index ae8ad093c9..b01d5675b2 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -19,12 +19,16 @@ Élie Soubiran, ... *) open Pp +open Errors open Util (** {6 Identifiers } *) type identifier = string +let check_ident_soft x = Option.iter Pp.warning (ident_refutation x) +let check_ident x = Option.iter Errors.error (ident_refutation x) + let id_of_string s = check_ident_soft s; String.copy s let string_of_id id = String.copy id diff --git a/kernel/names.mli b/kernel/names.mli index 34c5e62c5a..63c64f364e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -10,6 +10,9 @@ type identifier +val check_ident : string -> unit +val check_ident_soft : string -> unit + (** Parsing and printing of identifiers *) val string_of_id : identifier -> string val id_of_string : string -> identifier diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 985aac95fe..ec4a2d195b 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -13,6 +13,7 @@ (* This file defines the type of kernel environments *) +open Errors open Util open Names open Sign diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 40ce887b2c..0d279bc39d 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Sign diff --git a/kernel/reduction.ml b/kernel/reduction.ml index fc5e32cf5c..10eccd059b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -15,6 +15,7 @@ (* Equal inductive types by Jacek Chrzaszcz as part of the module system, Aug 2002 *) +open Errors open Util open Names open Term diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c2d71ebb27..e87bc9c1c1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -57,6 +57,7 @@ etc. *) +open Errors open Util open Names open Univ diff --git a/kernel/sign.ml b/kernel/sign.ml index 71169563b9..861cb0b6c5 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -16,6 +16,7 @@ names-based contexts *) open Names +open Errors open Util open Term diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c141a02aa3..9fb0454077 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -12,6 +12,7 @@ (* This module checks subtyping of module types *) (*i*) +open Errors open Util open Names open Univ @@ -278,7 +279,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Declarations.force lc2 in check_conv NotConvertibleBodyField cst conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -289,7 +290,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index dcb63cf7b8..0a4782d8c1 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -23,6 +23,7 @@ Inductive Constructions (CIC) terms together with constructors, destructors, iterators and basic functions *) +open Errors open Util open Pp open Names diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 478b9c6fc6..887a900100 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -12,6 +12,7 @@ (* This module provides the main entry points for type-checking basic declarations *) +open Errors open Util open Names open Univ diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 49106c9125..a2dd099766 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/univ.ml b/kernel/univ.ml index 0193542a36..d967846f18 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -14,6 +14,7 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) open Pp +open Errors open Util (* Universes are stratified by a partial ordering $\le$. @@ -817,9 +818,9 @@ let pr_arc = function | _, Canonical {univ=u; lt=lt; le=le} -> pr_uni_level u ++ str " " ++ v 0 - (prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++ + (pr_sequence (fun v -> str "< " ++ pr_uni_level v) lt ++ (if lt <> [] & le <> [] then spc () else mt()) ++ - prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++ + pr_sequence (fun v -> str "<= " ++ pr_uni_level v) le) ++ fnl () | u, Equiv v -> pr_uni_level u ++ str " = " ++ pr_uni_level v ++ fnl () diff --git a/kernel/vm.ml b/kernel/vm.ml index 86aed5d939..851b66d489 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -224,7 +224,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work") + | _ -> Errors.anomaly "Vm.whd : kind_of_closure does not work") else Vconstr_block(Obj.obj o) |