diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 18 | ||||
| -rw-r--r-- | library/goptions.ml | 10 |
3 files changed, 25 insertions, 6 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index 04ee14fb53..ab07b3647e 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -205,7 +205,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> (iter_array e1_array) ** (iter_array e2_array) | Const (kn,_) -> do_memoize_kn kn - | _ -> identity2 (* closed atomic types + rel *) + | Proj (_, e) -> iter e + | Rel _ | Sort _ | Ind _ | Construct _ -> identity2 and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2 in iter t s acc diff --git a/library/global.mli b/library/global.mli index af23d9b72c..62d7ea3210 100644 --- a/library/global.mli +++ b/library/global.mli @@ -118,9 +118,23 @@ val is_template_polymorphic : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context -val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant in its global or local universe + context. The type should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) -(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant, forgetting its universe context if + it is polymorphic, use with care: for polymorphic constants, the + type cannot be used to produce a term used by the kernel. For safe + handling of polymorphic global references, one should look at a + particular instantiation of the reference, in some particular + universe context (part of an [env] or [evar_map]), see + e.g. [type_of_constant_in]. If you want to create a fresh instance + of the reference and get its type look at [Evd.fresh_global] or + [Evarutil.new_global] and [Retyping.get_type_of]. *) + +(** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : Globnames.global_reference -> Univ.universe_context (** {6 Retroknowledge } *) diff --git a/library/goptions.ml b/library/goptions.ml index 4aea33685e..ef25fa5902 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -268,10 +268,14 @@ let declare_option cast uncast begin fun v -> add_anonymous_leaf (gdecl_obj v) end else write,write,write in + let warn () = + if depr then + msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") + in let cread () = cast (read ()) in - let cwrite v = write (uncast v) in - let clwrite v = lwrite (uncast v) in - let cgwrite v = gwrite (uncast v) in + let cwrite v = warn (); write (uncast v) in + let clwrite v = warn (); lwrite (uncast v) in + let cgwrite v = warn (); gwrite (uncast v) in value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab; write |