diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 4 | ||||
| -rw-r--r-- | kernel/closure.mli | 4 | ||||
| -rw-r--r-- | kernel/modops.ml | 11 | ||||
| -rw-r--r-- | kernel/modops.mli | 5 | ||||
| -rw-r--r-- | kernel/names.ml | 5 | ||||
| -rw-r--r-- | kernel/names.mli | 5 | ||||
| -rw-r--r-- | kernel/term.ml | 4 | ||||
| -rw-r--r-- | kernel/term.mli | 4 |
8 files changed, 25 insertions, 17 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 078f46b8d6..c3b828a39d 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -52,10 +52,6 @@ let with_stats c = end else Lazy.force c -type evaluable_global_reference = - | EvalVarRef of identifier - | EvalConstRef of constant - type transparent_state = Idpred.t * KNpred.t let all_opaque = (Idpred.empty, KNpred.empty) diff --git a/kernel/closure.mli b/kernel/closure.mli index d3c5e5c59f..4442e49f9f 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -22,10 +22,6 @@ val share : bool ref val with_stats: 'a Lazy.t -> 'a -type evaluable_global_reference = - | EvalVarRef of identifier - | EvalConstRef of kernel_name - (*s Delta implies all consts (both global (= by [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of diff --git a/kernel/modops.ml b/kernel/modops.ml index 758bf21596..a75f2d4832 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -10,6 +10,7 @@ (*i*) open Util +open Pp open Names open Univ open Term @@ -51,11 +52,13 @@ let error_no_module_to_end _ = let error_no_modtype_to_end _ = error "No open module type to end" -let error_not_a_modtype s = - error ("\""^s^"\" is not a module type") +let error_not_a_modtype_loc loc s = + user_err_loc (loc,"",str ("\""^s^"\" is not a module type")) -let error_not_a_module s = - error ("\""^s^"\" is not a module") +let error_not_a_module_loc loc s = + 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") diff --git a/kernel/modops.mli b/kernel/modops.mli index 68f8ea38aa..e865159c5b 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -9,6 +9,7 @@ (*i $Id$ i*) (*i*) +open Util open Names open Univ open Environ @@ -80,7 +81,9 @@ val error_no_module_to_end : unit -> 'a val error_no_modtype_to_end : unit -> 'a -val error_not_a_modtype : string -> 'a +val error_not_a_modtype_loc : loc -> string -> 'a + +val error_not_a_module_loc : loc -> string -> 'a val error_not_a_module : string -> 'a diff --git a/kernel/names.ml b/kernel/names.ml index 402e321d06..c9a1aa2ae8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -260,6 +260,11 @@ let ith_constructor_of_inductive ind i = (ind,i) let inductive_of_constructor (ind,i) = ind let index_of_constructor (ind,i) = i +(* Better to have it here that in closure, since used in grammar.cma *) +type evaluable_global_reference = + | EvalVarRef of identifier + | EvalConstRef of constant + (* Hash-consing of name objects *) module Hname = Hashcons.Make( struct diff --git a/kernel/names.mli b/kernel/names.mli index d9b9ddc9cd..2ecdd602d8 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -157,6 +157,11 @@ val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int +(* Better to have it here that in Closure, since required in grammar.cma *) +type evaluable_global_reference = + | EvalVarRef of identifier + | EvalConstRef of constant + (* Hash-consing *) val hcons_names : unit -> (kernel_name -> kernel_name) * (dir_path -> dir_path) * diff --git a/kernel/term.ml b/kernel/term.ml index cc6404631b..47bd656aea 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -22,11 +22,11 @@ type existential_key = int (* This defines Cases annotations *) type pattern_source = DefaultPat of int | RegularPat -type case_style = PrintLet | PrintIf | PrintCases +type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle type case_printing = { cnames : identifier array; ind_nargs : int; (* number of real args of the inductive type *) - style : case_style option; + style : case_style; source : pattern_source array } type case_info = { ci_ind : inductive; diff --git a/kernel/term.mli b/kernel/term.mli index 6da9d1f5f4..1867cc4505 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -37,11 +37,11 @@ type existential_key = int (*s Case annotation *) type pattern_source = DefaultPat of int | RegularPat -type case_style = PrintLet | PrintIf | PrintCases +type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle type case_printing = { cnames : identifier array; ind_nargs : int; (* number of real args of the inductive type *) - style : case_style option; + style : case_style; source : pattern_source array } (* the integer is the number of real args, needed for reduction *) type case_info = |