From bde492270970223482c77ac1605590b03720e613 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 16 Feb 2015 20:38:01 +0100 Subject: Comment on the unsafe_ functions in Global. --- library/global.mli | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/global.mli b/library/global.mli index af23d9b72c..ebf701acd8 100644 --- a/library/global.mli +++ b/library/global.mli @@ -116,11 +116,23 @@ val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool +(** 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. *) + val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context + +(** 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 needs an + accompanying [evar_map], see [Evd.fresh_global] and [Evarutil.new_global]. *) + val type_of_global_unsafe : Globnames.global_reference -> Constr.types -(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +(** 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 } *) -- cgit v1.2.3 From 4358f0e93885eb77c1513d4d606e386fb22b068e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 16 Feb 2015 20:47:38 +0100 Subject: Better comment for [type_of_global_unsafe]. --- library/global.mli | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) (limited to 'library') diff --git a/library/global.mli b/library/global.mli index ebf701acd8..62d7ea3210 100644 --- a/library/global.mli +++ b/library/global.mli @@ -116,21 +116,23 @@ val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool -(** 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. *) - val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context - -(** 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 needs an - accompanying [evar_map], see [Evd.fresh_global] and [Evarutil.new_global]. *) +(** 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. *) 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 -- cgit v1.2.3 From df3d820b45695e273515f8d7cf7c0345c7d574c5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Feb 2015 16:28:48 +0100 Subject: Fixing bug #4053. --- library/assumptions.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'library') 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 -- cgit v1.2.3 From 0b53955bb2bec43454ccbd317a09787a24fff3ae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Feb 2015 23:29:06 +0100 Subject: Deprecated options issue a warning. --- library/goptions.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'library') 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 -- cgit v1.2.3