Merge branch 'v8.5'

3 files changed, 5 insertions, 7 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f7ae30e7af..ba14f65d9e 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -122,7 +122,7 @@ let add_kn_delta_resolver kn kn' =
 
 let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
 
-(** Extending a [substitution] *)
+(** Extending a [substitution] without sequential composition *)
 
 let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s
 let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index fc2b0441ca..cd9fa79216 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -68,8 +68,9 @@ val empty_subst : substitution
 
 val is_empty_subst : substitution -> bool
 
-(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
-   sequential composition  *)
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential
+   composition. Most often this is not what you want. For sequential
+   composition, try [join (map_mbid mp delta) subs] **)
 val add_mbid :
   MBId.t -> module_path -> delta_resolver  -> substitution -> substitution
 val add_mp :
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 907ad2a1d4..55e767321b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -81,8 +81,7 @@ open Declarations
       These fields could be deduced from [revstruct], but they allow faster
       name freshness checks.
  - [univ] and [future_cst] : current and future universe constraints
- - [engagement] : are we Set-impredicative?
- - [type_in_type] : does the universe hierarchy collapse?
+ - [engagement] : are we Set-impredicative? does the universe hierarchy collapse?
  - [required] : names and digests of Require'd libraries since big-bang.
       This field will only grow
  - [loads] : list of libraries Require'd inside the current module.
@@ -122,7 +121,6 @@ type safe_environment =
     univ : Univ.constraints;
     future_cst : Univ.constraints Future.computation list;
     engagement : engagement option;
-    type_in_type : bool;
     required : vodigest DPMap.t;
     loads : (module_path * module_body) list;
     local_retroknowledge : Retroknowledge.action list;
@@ -152,7 +150,6 @@ let empty_environment =
     future_cst = [];
     univ = Univ.Constraint.empty;
     engagement = None;
-    type_in_type = false;
     required = DPMap.empty;
     loads = [];
     local_retroknowledge = [];