Merge branch 'v8.5'

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