Imported Upstream version 8.5~beta3+dfsg

1 files changed, 38 insertions, 21 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7..429aba4f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
 
-let type_in_type env = env.env_stratification.env_type_in_type
-
 let is_impredicative_set env = 
-  match engagement env with
-  | Some ImpredicativeSet -> true
+  match fst (engagement env) with
+  | ImpredicativeSet -> true
+  | _ -> false
+
+let type_in_type env =
+  match snd (engagement env) with
+  | TypeInType -> true
   | _ -> false
 
 let universes env = env.env_stratification.env_universes
@@ -159,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val
 let pop_rel_context n env =
   let ctxt = env.env_rel_context in
   { env with
-    env_rel_context = List.firstn (List.length ctxt - n) ctxt;
+    env_rel_context = List.skipn n ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
 let fold_named_context f env ~init =
@@ -178,30 +181,44 @@ let fold_named_context_reverse f ~init env =
 
 (* Universe constraints *)
 
-let add_constraints c env =
-  if Univ.Constraint.is_empty c then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+				     
+let add_constraints c env =
+  if Univ.Constraint.is_empty c then env
+  else map_universes (Univ.merge_constraints c) env
 
 let check_constraints c env =
   Univ.check_constraints c env.env_stratification.env_universes
 
-let set_engagement c env = (* Unsafe *)
-  { env with env_stratification =
-    { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
-  { env with env_stratification =
-    { env.env_stratification with env_type_in_type = true } }
-
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
-let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
+let add_universes strict ctx g =
+  let g = Array.fold_left
+	    (* Be lenient, module typing reintroduces universes and constraints due to includes *)
+	    (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+  in
+    Univ.merge_constraints (Univ.UContext.constraints ctx) g
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (add_universes strict ctx) env
+
+let add_universes_set strict ctx g =
+  let g = Univ.LSet.fold
+	    (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    (Univ.ContextSet.levels ctx) g
+  in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (add_universes_set strict ctx) env
+
+let set_engagement c env = (* Unsafe *)
+  { env with env_stratification =
+    { env.env_stratification with env_engagement = c } }
 
 (* Global constants *)