1 files changed, 60 insertions, 33 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7456ecea56..1bb2d3c79c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -319,6 +319,52 @@ let check_fixpoint env lna lar vdef vdeft =
   with NotConvertibleVect i ->
     error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar
 
+(* Global references *)
+
+let type_of_global_in_context env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = Environ.lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    cb.Declarations.const_type, univs
+  | IndRef ind ->
+    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
+    Inductive.type_of_inductive env (specif, inst), univs
+  | ConstructRef cstr ->
+    let (mib,_ as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    Inductive.type_of_constructor (cstr,inst) specif, univs
+
+(* Build a fresh instance for a given context, its associated substitution and
+   the instantiated constraints. *)
+
+let constr_of_global_in_context env r =
+  let open GlobRef in
+  match r with
+  | VarRef id -> mkVar id, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    mkConstU (c, Univ.make_abstract_instance univs), univs
+  | IndRef ind ->
+    let (mib,_) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkIndU (ind, Univ.make_abstract_instance univs), univs
+  | ConstructRef cstr ->
+    let (mib,_) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
+
 (************************************************************************)
 (************************************************************************)
 
@@ -432,21 +478,8 @@ and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
 
-let universe_levels_of_constr _env c =
-  let rec aux s c =
-    match kind c with
-    | Const (_c, u) ->
-       LSet.fold LSet.add (Instance.levels u) s
-    | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
-       LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) ->
-      let u = Sorts.univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> Constr.fold aux s c
-  in aux LSet.empty c
-
 let check_wellformed_universes env c =
-  let univs = universe_levels_of_constr env c in
+  let univs = universes_of_constr c in
   try UGraph.check_declared_universes (universes env) univs
   with UGraph.UndeclaredLevel u ->
     error_undeclared_universe env u
@@ -482,25 +515,19 @@ let infer_v env cv =
 
 (* Typing of several terms. *)
 
-let infer_local_decl env id = function
-  | Entries.LocalDefEntry c ->
-      let () = check_wellformed_universes env c in
-      let t = execute env c in
-      RelDecl.LocalDef (Name id, c, t)
-  | Entries.LocalAssumEntry c ->
-      let () = check_wellformed_universes env c in
-      let t = execute env c in
-      RelDecl.LocalAssum (Name id, check_assumption env c t)
-
-let infer_local_decls env decls =
-  let rec inferec env = function
-  | (id, d) :: l ->
-      let (env, l) = inferec env l in
-      let d = infer_local_decl env id d in
-        (push_rel d env, Context.Rel.add d l)
-  | [] -> (env, Context.Rel.empty)
-  in
-  inferec env decls
+let check_context env rels =
+  let open Context.Rel.Declaration in
+  Context.Rel.fold_outside (fun d env ->
+    match d with
+      | LocalAssum (_,ty) ->
+        let _ = infer_type env ty in
+        push_rel d env
+      | LocalDef (_,bd,ty) ->
+        let j1 = infer env bd in
+        let _ = infer_type env ty in
+        conv_leq false env j1.uj_type ty;
+        push_rel d env)
+    rels ~init:env
 
 let judge_of_prop = make_judge mkProp type1
 let judge_of_set = make_judge mkSet type1