From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 checker/mod_checking.ml | 60 +++++++++++++++++++------------------------------
 1 file changed, 23 insertions(+), 37 deletions(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7f93e156..3ef2b340 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -1,9 +1,7 @@
-
 open Pp
 open Util
 open Names
 open Cic
-open Term
 open Reduction
 open Typeops
 open Indtypes
@@ -14,51 +12,39 @@ open Environ
 
 (** {6 Checking constants } *)
 
-let refresh_arity ar =
-  let ctxt, hd = decompose_prod_assum ar in
-  match hd with
-      Sort (Type u) when not (Univ.is_univ_variable u) ->
-      let ul = Univ.Level.make DirPath.empty 1 in
-      let u' = Univ.Universe.make ul in
-      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
-      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
-        mkArity (ctxt,Prop Null), ctx
-    | _ -> ar, Univ.ContextSet.empty
-
 let check_constant_declaration env kn cb =
-  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
+  Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  (** Locally set the oracle for further typechecking *)
+  let oracle = env.env_conv_oracle in
+  let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
+  (** [env'] contains De Bruijn universe variables *)
   let env' =
-    if cb.const_polymorphic then
-      let inst = Univ.make_abstract_instance cb.const_universes in
-      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
-        push_context ~strict:false ctx env
-    else push_context ~strict:true cb.const_universes env
-  in
-  let envty, ty = 
-    match cb.const_type with
-      RegularArity ty ->
-        let ty', cu = refresh_arity ty in
-        let envty = push_context_set cu env' in
-        let _ = infer_type envty ty' in envty, ty
-    | TemplateArity(ctxt,par) ->
-        let _ = check_ctxt env' ctxt in
-        check_polymorphic_arity env' ctxt par;
-	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
+    match cb.const_universes with
+    | Monomorphic_const ctx -> push_context_set ~strict:true ctx env
+    | Polymorphic_const auctx ->
+      let ctx = Univ.AUContext.repr auctx in
+      push_context ~strict:false ctx env
   in
+  let ty = cb.const_type in
+  let () = ignore(infer_type env' ty) in
   let () = 
     match body_of_constant cb with
     | Some bd ->
       (match cb.const_proj with 
-      | None -> let j = infer envty bd in
-		  conv_leq envty j ty
+      | None -> let j = infer env' bd in
+                  conv_leq env' j ty
       | Some pb -> 
 	let env' = add_constant kn cb env' in
 	let j = infer env' bd in
-	  conv_leq envty j ty)
+          conv_leq env' j ty)
     | None -> ()
   in
-  if cb.const_polymorphic then add_constant kn cb env
-  else add_constant kn cb env'
+  let env =
+    if constant_is_polymorphic cb then add_constant kn cb env
+    else add_constant kn cb env'
+  in
+  (** Reset the value of the oracle *)
+  Environ.set_oracle env oracle
 
 (** {6 Checking modules } *)
 
@@ -74,12 +60,12 @@ let lookup_module mp env =
 
 let mk_mtb mp sign delta =
   { mod_mp = mp;
-    mod_expr = Abstract;
+    mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
     mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
-    mod_retroknowledge = []; }
+    mod_retroknowledge = ModTypeRK; }
 
 let rec check_module env mp mb =
   let (_:module_signature) =
-- 
cgit v1.2.3