Merge PR#613: Cumulativity for inductive types

1 files changed, 11 insertions, 9 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7f93e15609..15e9ae2951 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -1,4 +1,3 @@
-
 open Pp
 open Util
 open Names
@@ -26,21 +25,23 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
-  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
+  Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  let env', u =
+    match cb.const_universes with
+    | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty
+    | Polymorphic_const auctx ->
+      let ctx = Univ.instantiate_univ_context auctx in
+      push_context ~strict:false ctx env, Univ.UContext.instance ctx
   in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
+        let ty = subst_instance_constr u ty in
         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) ->
+        assert(Univ.Instance.is_empty u);
         let _ = check_ctxt env' ctxt in
         check_polymorphic_arity env' ctxt par;
 	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
@@ -48,6 +49,7 @@ let check_constant_declaration env kn cb =
   let () = 
     match body_of_constant cb with
     | Some bd ->
+      let bd = subst_instance_constr u bd in
       (match cb.const_proj with 
       | None -> let j = infer envty bd in
 		  conv_leq envty j ty
@@ -57,7 +59,7 @@ let check_constant_declaration env kn cb =
 	  conv_leq envty j ty)
     | None -> ()
   in
-  if cb.const_polymorphic then add_constant kn cb env
+  if constant_is_polymorphic cb then add_constant kn cb env
   else add_constant kn cb env'
 
 (** {6 Checking modules } *)