From 0d9a91113c4112eece0680e433f435fdfb39ea4b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Jul 2017 16:33:47 +0200
Subject: Getting rid of simple calls to AUContext.instance.

This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
---
 checker/inductive.ml      |  7 -------
 checker/inductive.mli     |  2 --
 checker/reduction.ml      |  8 ++++----
 checker/subtyping.ml      | 20 +++++---------------
 checker/univ.ml           |  1 +
 checker/univ.mli          |  1 +
 engine/universes.ml       | 19 +++++++++----------
 kernel/cooking.ml         | 11 ++++++-----
 kernel/indtypes.ml        |  7 ++-----
 kernel/nativecode.ml      | 10 +++++-----
 kernel/reduction.ml       |  6 ++----
 kernel/term_typing.ml     |  5 ++---
 library/lib.ml            |  3 ++-
 library/univops.ml        | 39 ---------------------------------------
 library/univops.mli       |  2 --
 pretyping/evarconv.ml     |  5 ++---
 pretyping/reductionops.ml |  8 ++++----
 17 files changed, 45 insertions(+), 109 deletions(-)

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 93ffa329a6..a145165aab 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -66,13 +66,6 @@ let inductive_is_cumulative mib =
   | Polymorphic_ind ctx -> false
   | Cumulative_ind cumi -> true
 
-let inductive_polymorphic_instance mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.Instance.empty
-  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
-  | Cumulative_ind cumi -> 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
-
 let inductive_polymorphic_context mib =
   match mib.mind_universes with
   | Monomorphic_ind _ -> Univ.UContext.empty
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 698b8b77c2..b8cbda7cf7 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -26,8 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool
 
 val inductive_is_cumulative : mutual_inductive_body -> bool
 
-val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance
-
 val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
 
 val type_of_inductive : env -> mind_specif puniverses -> constr
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 93b8b907ca..0b605820d7 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -157,11 +157,11 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
   else raise NotConvertible
 
 let convert_inductive_instances cv_pb cumi u u' univs =
-  let ind_instance =
-      Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in
+  let len_instance =
+      Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
   let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+  if not ((len_instance = Univ.Instance.length u) &&
+          (len_instance = Univ.Instance.length u')) then
     anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5fd5510a7f..303b18476d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -309,27 +309,17 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		let c2 = force_constr lc2 in
 		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
-	  ignore (CErrors.user_err (Pp.str (
+        CErrors.user_err (Pp.str (
 		    "The kernel does not recognize yet that a parameter can be " ^
 		      "instantiated by an inductive type. Hint: you can rename the " ^
 		      "inductive type and give a definition to map the old name to the new " ^
-		      "name.")));
-      if constant_has_body cb2 then error () ;
-      let u = inductive_polymorphic_instance mind1 in
-      let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
-      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv conv_leq env arity1 typ2
-   | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (CErrors.user_err (Pp.str (
+		      "name."))
+   | IndConstr (((kn,i),j),mind1) ->
+      CErrors.user_err (Pp.str (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
-       "name.")));
-      if constant_has_body cb2 then error () ;
-      let u1 = inductive_polymorphic_instance mind1 in
-      let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
-      let ty2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv conv env ty1 ty2
+       "name."))
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
diff --git a/checker/univ.ml b/checker/univ.ml
index b434db129e..4eebcb25b9 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1175,6 +1175,7 @@ struct
   let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
+  let size (univs, _) = Instance.length univs
 
   let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
   let pr prl (univs, cst as ctx) =
diff --git a/checker/univ.mli b/checker/univ.mli
index 457ccbdfff..faa682cbf0 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -209,6 +209,7 @@ sig
   type t
 
   val instance : t -> Instance.t
+  val size : t -> int
 
 end
 
diff --git a/engine/universes.ml b/engine/universes.ml
index 28058aeed8..5df02c8a95 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -282,8 +282,8 @@ let new_Type dp = mkType (new_univ dp)
 let new_Type_sort dp = Type (new_univ dp)
 
 let fresh_universe_instance ctx =
-  Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) 
-    (AUContext.instance ctx)
+  let init _ = new_univ_level (Global.current_dirpath ()) in
+  Instance.of_array (Array.init (AUContext.size ctx) init)
 
 let fresh_instance_from_context ctx =
   let inst = fresh_universe_instance ctx in
@@ -292,18 +292,17 @@ let fresh_instance_from_context ctx =
 
 let fresh_instance ctx =
   let ctx' = ref LSet.empty in
-  let inst = 
-    Instance.subst_fn (fun v -> 
-      let u = new_univ_level (Global.current_dirpath ()) in
-	ctx' := LSet.add u !ctx'; u) 
-      (AUContext.instance ctx)
+  let init _ =
+    let u = new_univ_level (Global.current_dirpath ()) in
+    ctx' := LSet.add u !ctx'; u
+  in
+  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
   in !ctx', inst
 
 let existing_instance ctx inst = 
   let () = 
-    let a1 = Instance.to_array inst 
-    and a2 = Instance.to_array (AUContext.instance ctx) in
-    let len1 = Array.length a1 and len2 = Array.length a2 in 
+    let len1 = Array.length (Instance.to_array inst)
+    and len2 = AUContext.size ctx in
       if not (len1 == len2) then
 	CErrors.user_err ~hdr:"Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b9e7ec1691..852f87d5e9 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -184,13 +184,14 @@ let lift_univs cb subst =
     if (Univ.LMap.is_empty subst) then
       subst, (Polymorphic_const auctx)
     else
-      let inst = Univ.AUContext.instance auctx in
       let len = Univ.LMap.cardinal subst in
-      let subst = 
-        Array.fold_left_i 
-          (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc)
-	  subst (Univ.Instance.to_array inst)
+      let rec gen_subst i acc =
+        if i < 0 then acc
+        else
+          let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in
+          gen_subst (pred i) acc
       in
+      let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in
       let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
       subst, (Polymorphic_const auctx')
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 04971f83dc..e248436ec4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -961,13 +961,10 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u =
-        let process auctx = 
-          subst_univs_level_instance substunivs (Univ.AUContext.instance auctx)
-        in
         match aiu with
         | Monomorphic_ind _ -> Univ.Instance.empty
-        | Polymorphic_ind auctx -> process auctx
-        | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi)
+        | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
+        | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
       in
       let indsp = ((kn, 0), u) in
       let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1acede729a..9d72622068 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1861,10 +1861,10 @@ and compile_named env sigma univ auxdefs id =
 let compile_constant env sigma prefix ~interactive con cb =
   match cb.const_proj with
   | None ->
-     let u =
+     let no_univs =
        match cb.const_universes with
-       | Monomorphic_const _ -> Univ.Instance.empty
-       | Polymorphic_const ctx -> Univ.AUContext.instance ctx
+       | Monomorphic_const _ -> true
+       | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0
      in
     begin match cb.const_body with
     | Def t ->
@@ -1879,7 +1879,7 @@ let compile_constant env sigma prefix ~interactive con cb =
       in
       let l = con_label con in
       let auxdefs,code =
-	if Univ.Instance.is_empty u then compile_with_fv env sigma None [] (Some l) code
+	if no_univs then compile_with_fv env sigma None [] (Some l) code
 	else
 	  let univ = fresh_univ () in
 	  let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
@@ -1894,7 +1894,7 @@ let compile_constant env sigma prefix ~interactive con cb =
     | _ -> 
         let i = push_symbol (SymbConst con) in
 	let args =
-	  if Univ.Instance.is_empty u then [|get_const_code i; MLarray [||]|]
+	  if no_univs then [|get_const_code i; MLarray [||]|]
 	  else [|get_const_code i|]
 	in
 	(*
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index de4efbba93..423e0d9349 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -680,8 +680,7 @@ let infer_check_conv_constructors
 
 let check_inductive_instances cv_pb cumi u u' univs =
   let length_ind_instance = 
-    Univ.Instance.length
-      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
   in
   let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((length_ind_instance = Univ.Instance.length u) &&
@@ -767,8 +766,7 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
 
 let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
   let length_ind_instance = 
-    Univ.Instance.length
-      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
   in
   let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((length_ind_instance = Univ.Instance.length u) &&
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 283febed24..eee227370e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -131,8 +131,7 @@ let inline_side_effects env body ctx side_eff =
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
       | Polymorphic_const auctx ->
         (** Inline the term to emulate universe polymorphism *)
-        let data = (Univ.AUContext.instance auctx, b) in
-        let subst = Cmap_env.add c (Inl data) subst in
+        let subst = Cmap_env.add c (Inl b) subst in
         (subst, var, ctx, args)
     in
     let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in
@@ -142,7 +141,7 @@ let inline_side_effects env body ctx side_eff =
       let data = try Some (Cmap_env.find c subst) with Not_found -> None in
       begin match data with
       | None -> t
-      | Some (Inl (inst, b)) ->
+      | Some (Inl b) ->
         (** [b] is closed but may refer to other constants *)
         subst_const i k (Vars.subst_instance_constr u b)
       | Some (Inr n) ->
diff --git a/library/lib.ml b/library/lib.ml
index 009eb88fc1..439f83578d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -465,9 +465,10 @@ let add_section_replacement f g poly hyps =
     let () = check_same_poly poly vars in
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
+    let inst = Univ.UContext.instance ctx in
     let subst, ctx = Univ.abstract_universes ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (Univ.AUContext.instance ctx,args) exps,
+    sectab := (vars,f (inst,args) exps,
 	      g (sechyps,subst,ctx) abs)::sl
 
 let add_section_kn poly kn =
diff --git a/library/univops.ml b/library/univops.ml
index 669be2d452..3bafb824d1 100644
--- a/library/univops.ml
+++ b/library/univops.ml
@@ -8,7 +8,6 @@
 
 open Term
 open Univ
-open Declarations
 
 let universes_of_constr c =
   let rec aux s c = 
@@ -21,44 +20,6 @@ let universes_of_constr c =
     | _ -> fold_constr aux s c
   in aux LSet.empty c
 
-let universes_of_inductive mind =
-  let process auctx =
-    let u = Univ.AUContext.instance auctx in
-    let univ_of_one_ind oind = 
-      let arity_univs =
-        Context.Rel.fold_outside
-          (fun decl unvs ->
-             Univ.LSet.union
-              (Context.Rel.Declaration.fold_constr
-                 (fun cnstr unvs ->
-                    let cnstr = Vars.subst_instance_constr u cnstr in
-                    Univ.LSet.union
-                      (universes_of_constr cnstr) unvs)
-              decl Univ.LSet.empty) unvs)
-        oind.mind_arity_ctxt ~init:Univ.LSet.empty
-      in
-      Array.fold_left (fun unvs cns ->
-          let cns = Vars.subst_instance_constr u cns in
-          Univ.LSet.union (universes_of_constr cns) unvs) arity_univs 
-       oind.mind_nf_lc
-    in
-    let univs = 
-      Array.fold_left
-        (fun unvs pk ->
-           Univ.LSet.union
-             (univ_of_one_ind pk) unvs
-        )
-        Univ.LSet.empty mind.mind_packets 
-    in
-    let mindcnt =  Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in
-    let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in
-    univs
-  in
-  match mind.mind_universes with
-  | Monomorphic_ind _ -> LSet.empty
-  | Polymorphic_ind auctx -> process auctx
-  | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi)
-
 let restrict_universe_context (univs,csts) s =
   (* Universes that are not necessary to typecheck the term.
      E.g. univs introduced by tactics and not used in the proof term. *)
diff --git a/library/univops.mli b/library/univops.mli
index b5f7715b11..09147cb41c 100644
--- a/library/univops.mli
+++ b/library/univops.mli
@@ -8,10 +8,8 @@
 
 open Term
 open Univ
-open Declarations
 
 (** Shrink a universe context to a restricted set of variables *)
 
 val universes_of_constr : constr -> universe_set
-val universes_of_inductive : mutual_inductive_body -> universe_set
 val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b5d195873c..2acf6bfe67 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,9 +353,8 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 let check_leq_inductives evd cumi u u' =
   let u = EConstr.EInstance.kind evd u in
   let u' = EConstr.EInstance.kind evd u' in
-  let length_ind_instance = 
-    Univ.Instance.length
-      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+  let length_ind_instance =
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
   in
   let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((length_ind_instance = Univ.Instance.length u) &&
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cc1709f1c2..3acefa1342 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1362,12 +1362,12 @@ let sigma_compare_instances ~flex i0 i1 sigma =
 	raise Reduction.NotConvertible
 
 let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
-  let ind_instance = 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) 
+  let len_instance =
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind)
   in
   let ind_sbctx =  Univ.ACumulativityInfo.subtyp_context uinfind  in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+  if not ((len_instance = Univ.Instance.length u) &&
+          (len_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
-- 
cgit v1.2.3


From 1309723672def9bf322a23e9c789e4a8bc2a4ac3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 16:56:10 +0200
Subject: Asserting that monomorphic section variables have no abstracted
 context.

---
 kernel/cooking.ml | 2 +-
 kernel/univ.mli   | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 852f87d5e9..95822fac68 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -250,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } =
   let univs =
     match univs with
     | Monomorphic_const ctx -> 
-      Monomorphic_const (UContext.union (instantiate_univ_context abs_ctx) ctx)
+      assert (AUContext.is_empty abs_ctx); univs
     | Polymorphic_const auctx -> 
       Polymorphic_const (AUContext.union abs_ctx auctx)
   in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index d7ee3eceec..dc6fb85a05 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -320,6 +320,7 @@ sig
   type t
 
   val empty : t
+  val is_empty : t -> bool
 
   val instance : t -> Instance.t
                         
-- 
cgit v1.2.3


From b8a7222e670f69e024d50394afd88204e15d1b29 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 18:05:23 +0200
Subject: Less footguns in universe handling: remove subst_instance_context.

This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
---
 checker/environ.ml        |  3 +-
 checker/reduction.ml      |  6 ++--
 checker/univ.ml           | 67 ++++++++++++++++++++++-------------------
 checker/univ.mli          |  3 +-
 engine/universes.ml       |  4 +--
 kernel/environ.ml         |  3 +-
 kernel/inductive.ml       |  4 +--
 kernel/reduction.ml       | 13 ++++----
 kernel/univ.ml            | 76 +++++++++++++++++++++--------------------------
 kernel/univ.mli           |  4 ++-
 pretyping/evarconv.ml     |  4 +--
 pretyping/reductionops.ml |  6 ++--
 12 files changed, 90 insertions(+), 103 deletions(-)

diff --git a/checker/environ.ml b/checker/environ.ml
index 11b8ea67cc..d3f393c651 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -122,8 +122,7 @@ type const_evaluation_result = NoBody | Opaque | IsProj
 let constraints_of cb u =
   match cb.const_universes with
   | Monomorphic_const _ -> Univ.Constraint.empty
-  | Polymorphic_const ctx -> 
-    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 0b605820d7..6d8783d7e5 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -166,16 +166,14 @@ let convert_inductive_instances cv_pb cumi u u' univs =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-      (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV ->
         let comp_cst' =
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints
-            (Univ.subst_instance_context comp_subst ind_subtypctx)
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
         in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
diff --git a/checker/univ.ml b/checker/univ.ml
index 4eebcb25b9..600af230c9 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1160,6 +1160,33 @@ struct
   
 end
 
+(** Substitute instance inst for ctx in csts *)
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1185,7 +1212,15 @@ end
 
 type universe_context = UContext.t
 
-module AUContext = UContext
+module AUContext =
+struct
+  include UContext
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
 
 type abstract_universe_context = AUContext.t
 
@@ -1264,36 +1299,6 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
-(** Substitute instance inst for ctx in csts *)
-
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty
-
-let subst_instance_context inst (inner_inst, inner_constr) =
-  (inner_inst, subst_instance_constraints inst inner_constr)
-
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
 
diff --git a/checker/univ.mli b/checker/univ.mli
index faa682cbf0..75c76cd129 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -211,6 +211,8 @@ sig
   val instance : t -> Instance.t
   val size : t -> int
 
+  val instantiate : Instance.t -> t -> Constraint.t
+
 end
 
 type abstract_universe_context = AUContext.t
@@ -277,7 +279,6 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
 
 (* val make_instance_subst : universe_instance -> universe_level_subst *)
 (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 5df02c8a95..fc441fd0b4 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -287,7 +287,7 @@ let fresh_universe_instance ctx =
 
 let fresh_instance_from_context ctx =
   let inst = fresh_universe_instance ctx in
-  let constraints = UContext.constraints (subst_instance_context inst ctx) in
+  let constraints = AUContext.instantiate inst ctx in
     inst, constraints
 
 let fresh_instance ctx =
@@ -316,7 +316,7 @@ let fresh_instance_from ctx inst =
     | Some inst -> existing_instance ctx inst
     | None -> fresh_instance ctx 
   in
-  let constraints = UContext.constraints (subst_instance_context inst ctx) in
+  let constraints = AUContext.instantiate inst ctx in
     inst, (ctx', constraints)
 
 let unsafe_instance_from ctx =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd204c7d59..ca2c8e1356 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -230,8 +230,7 @@ let add_constant kn cb env =
 let constraints_of cb u =
   match cb.const_universes with
   | Monomorphic_const _ -> Univ.Constraint.empty
-  | Polymorphic_const ctx -> 
-    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3fb472be1..1eaba49aa9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,9 +54,7 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  let process auctx = 
-    Univ.UContext.constraints (Univ.subst_instance_context u auctx)
-  in
+  let process auctx =  Univ.AUContext.instantiate u auctx in
   match mib.mind_universes with
   | Monomorphic_ind _ -> Univ.Constraint.empty
   | Polymorphic_ind auctx -> process auctx
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 423e0d9349..2bf9f43a5a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -689,16 +689,14 @@ let check_inductive_instances cv_pb cumi u u' univs =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-        (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
         let comp_cst' = 
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints 
-            (Univ.subst_instance_context comp_subst ind_subtypctx) 
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
         in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
@@ -775,16 +773,15 @@ let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-        (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
         let comp_cst' = 
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints
-            (Univ.subst_instance_context comp_subst ind_subtypctx) in
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1c887e2a99..cb19761b32 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -988,6 +988,31 @@ let enforce_eq_instances x y =
 		 (Pp.str " instances of different lengths."));
     CArray.fold_right2 enforce_eq_level ax ay
 
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty 
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1031,7 +1056,15 @@ end
 type universe_context = UContext.t
 let hcons_universe_context = UContext.hcons
 
-module AUContext = UContext
+module AUContext =
+struct
+  include UContext
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
 
 type abstract_universe_context = AUContext.t
 let hcons_abstract_universe_context = AUContext.hcons
@@ -1256,31 +1289,6 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty 
 
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
-
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
@@ -1378,19 +1386,3 @@ let explain_universe_inconsistency prl (o,u,v,p) =
 let compare_levels = Level.compare
 let eq_levels = Level.equal
 let equal_universes = Universe.equal
-
-
-let subst_instance_constraints = 
-  if Flags.profile then 
-    let key = Profile.declare_profile "subst_instance_constraints" in
-      Profile.profile2 key subst_instance_constraints
-  else subst_instance_constraints
-
-let subst_instance_context = 
-  let subst_instance_context_body inst (inner_inst, inner_constr) =
-    (inner_inst, subst_instance_constraints inst inner_constr)
-  in
-  if Flags.profile then 
-    let key = Profile.declare_profile "subst_instance_constraints" in
-      Profile.profile2 key subst_instance_context_body
-  else subst_instance_context_body
diff --git a/kernel/univ.mli b/kernel/univ.mli
index dc6fb85a05..3d0d2234dc 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -329,6 +329,9 @@ sig
   (** Keeps the order of the instances *)
   val union : t -> t -> t
 
+  val instantiate : Instance.t -> t -> Constraint.t
+  (** Generate the set of instantiated constraints **)
+
 end
 
 type abstract_universe_context = AUContext.t
@@ -443,7 +446,6 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
 
 val make_instance_subst : universe_instance -> universe_level_subst
 val make_inverse_instance_subst : universe_instance -> universe_level_subst
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2acf6bfe67..87f29ba492 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -363,9 +363,7 @@ let check_leq_inductives evd cumi u u' =
   else
     begin
      let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = 
-       Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
-     in
+     let comp_cst =  Univ.AUContext.instantiate comp_subst ind_sbcst in
      Evd.add_constraints evd comp_cst
     end
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3acefa1342..21ed8e0a23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1372,15 +1372,13 @@ let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx)
+      Univ.AUContext.instantiate comp_subst ind_sbctx
     in
     let comp_cst =
       match cv_pb with
         Reduction.CONV -> 
         let comp_subst = (Univ.Instance.append u' u) in
-        let comp_cst' = 
-          Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
-        in
+        let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in
         Univ.Constraint.union comp_cst comp_cst'
       | Reduction.CUMUL -> comp_cst
     in
-- 
cgit v1.2.3


From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 19:11:20 +0200
Subject: Safe API for accessing universe constraints of global references.

Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
---
 checker/inductive.ml     |  7 -------
 checker/inductive.mli    |  2 --
 kernel/declareops.ml     | 28 +++++-----------------------
 kernel/declareops.mli    |  9 ++-------
 kernel/environ.ml        | 10 ++--------
 kernel/environ.mli       |  5 +----
 kernel/nativecode.ml     |  4 ++--
 library/global.ml        | 48 ++++++++++++++++++++++++------------------------
 library/global.mli       |  2 +-
 pretyping/recordops.ml   |  5 +++--
 pretyping/typeclasses.ml |  4 ++--
 pretyping/vnorm.ml       |  4 ++--
 printing/prettyp.ml      |  7 ++++++-
 printing/printmod.ml     | 15 +++++++++------
 tactics/elimschemes.ml   |  6 ++++--
 vernac/obligations.ml    |  2 +-
 vernac/record.ml         |  4 ++--
 vernac/search.ml         |  2 +-
 18 files changed, 67 insertions(+), 97 deletions(-)

diff --git a/checker/inductive.ml b/checker/inductive.ml
index a145165aab..1271a02b0e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -66,13 +66,6 @@ let inductive_is_cumulative mib =
   | Polymorphic_ind ctx -> false
   | Cumulative_ind cumi -> true
 
-let inductive_polymorphic_context mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.UContext.empty
-  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
-  | Cumulative_ind cumi -> 
-    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
-
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
diff --git a/checker/inductive.mli b/checker/inductive.mli
index b8cbda7cf7..8f605935db 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -26,8 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool
 
 val inductive_is_cumulative : mutual_inductive_body -> bool
 
-val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
-
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
 (* Return type as quoted by the user *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1337036b8b..cf6d3c55e1 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -67,24 +67,14 @@ let type_of_constant cb =
       if t' == t then x else RegularArity t'
   | TemplateArity _ as x -> x
 
-let universes_of_polymorphic_constant otab cb = 
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
-
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
   | Def _ | OpaqueDef _ -> true
 
-let constant_polymorphic_instance cb =
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Instance.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
-
 let constant_polymorphic_context cb =
   match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+  | Monomorphic_const _ -> Univ.AUContext.empty
+  | Polymorphic_const ctx -> ctx
 
 let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
@@ -268,19 +258,11 @@ let subst_mind_body sub mib =
     mind_typing_flags = mib.mind_typing_flags;
   }
 
-let inductive_polymorphic_instance mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.Instance.empty
-  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
-  | Cumulative_ind cumi -> 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
-
 let inductive_polymorphic_context mib =
   match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.UContext.empty
-  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
-  | Cumulative_ind cumi -> 
-    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+  | Monomorphic_ind _ -> Univ.AUContext.empty
+  | Polymorphic_ind ctx -> ctx
+  | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi
 
 let inductive_is_polymorphic mib =
   match mib.mind_universes with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 7350724b8b..987c1adaf1 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -27,8 +27,7 @@ val subst_const_body : substitution -> constant_body -> constant_body
 
 val constant_has_body : constant_body -> bool
 
-val constant_polymorphic_instance : constant_body -> universe_instance
-val constant_polymorphic_context : constant_body -> universe_context
+val constant_polymorphic_context : constant_body -> abstract_universe_context
 
 (** Is the constant polymorphic? *)
 val constant_is_polymorphic : constant_body -> bool
@@ -43,9 +42,6 @@ val type_of_constant : constant_body -> constant_type
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
-val universes_of_polymorphic_constant :
-  Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
-
 val is_opaque : constant_body -> bool
 
 (** Side effects *)
@@ -68,8 +64,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance
-val inductive_polymorphic_context : mutual_inductive_body -> universe_context
+val inductive_polymorphic_context : mutual_inductive_body -> abstract_universe_context
 
 (** Is the inductive polymorphic? *)
 val inductive_is_polymorphic : mutual_inductive_body -> bool
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ca2c8e1356..b01b652001 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -247,17 +247,11 @@ let constant_type env (kn,u) =
     let csts = constraints_of cb u in
     (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
 
-let constant_instance env kn =
-  let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Instance.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instance ctx
-
 let constant_context env kn =
   let cb = lookup_constant kn env in
   match cb.const_universes with
-  | Monomorphic_const _ -> Univ.UContext.empty
-  | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+  | Monomorphic_const _ -> Univ.AUContext.empty
+  | Polymorphic_const ctx -> ctx
 
 type const_evaluation_result = NoBody | Opaque | IsProj
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f8887d8e83..cd7a9d2791 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -160,10 +160,7 @@ val constant_value_and_type : env -> constant puniverses ->
   constr option * constant_type * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
-val constant_context : env -> constant -> Univ.universe_context
-(** The universe isntance associated to the constant, empty if not 
-    polymorphic *)
-val constant_instance : env -> constant -> Univ.universe_instance
+val constant_context : env -> constant -> Univ.abstract_universe_context
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9d72622068..da7fcd6f23 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1959,14 +1959,14 @@ let param_name = Name (id_of_string "params")
 let arg_name = Name (id_of_string "arg")
 
 let compile_mind prefix ~interactive mb mind stack =
-  let u = Declareops.inductive_polymorphic_instance mb in
+  let u = Declareops.inductive_polymorphic_context mb in
   let f i stack ob =
     let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
     let j = push_symbol (SymbInd (mind,i)) in
     let name = Gind ("", (mind, i)) in
     let accu =
       let args =
-	if Univ.Instance.is_empty u then
+	if Int.equal (Univ.AUContext.size u) 0 then
 	  [|get_ind_code j; MLarray [||]|]
 	else [|get_ind_code j|]
       in
diff --git a/library/global.ml b/library/global.ml
index 8b59c84dda..09c202c500 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -164,49 +164,49 @@ let type_of_global_unsafe r =
   match r with
   | VarRef id -> Environ.named_type id env
   | ConstRef c -> 
-     let cb = Environ.lookup_constant c env in 
-     let univs =
-       Declareops.universes_of_polymorphic_constant
-         (Environ.opaque_tables env) cb in
-     let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
-       Vars.subst_instance_constr (Univ.UContext.instance univs) ty
+    let cb = Environ.lookup_constant c env in 
+    let inst = Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) in
+    let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
+    Vars.subst_instance_constr inst ty
   | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let inst = Declareops.inductive_polymorphic_instance mib in
-       Inductive.type_of_inductive env (specif, inst)
+    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
+    Inductive.type_of_inductive env (specif, inst)
   | ConstructRef cstr ->
-     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-     let inst = Declareops.inductive_polymorphic_instance mib in
-     Inductive.type_of_constructor (cstr,inst) specif
+    let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
+    Inductive.type_of_constructor (cstr,inst) specif
 
 let type_of_global_in_context env r = 
   match r with
   | VarRef id -> Environ.named_type id env, Univ.UContext.empty
   | ConstRef c -> 
-     let cb = Environ.lookup_constant c env in 
-     let univs =
-       Declareops.universes_of_polymorphic_constant
-         (Environ.opaque_tables env) cb in
-       Typeops.type_of_constant_type env cb.Declarations.const_type, univs
+    let cb = Environ.lookup_constant c env in 
+    let univs = Declareops.constant_polymorphic_context cb in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let univs = Declareops.inductive_polymorphic_context mib in
-     Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
+    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    Inductive.type_of_inductive env (specif, inst), univs
   | ConstructRef cstr ->
     let (mib,oib as specif) =
       Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
     in
     let univs = Declareops.inductive_polymorphic_context mib in
-    let inst = Univ.UContext.instance univs in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
     Inductive.type_of_constructor (cstr,inst) specif, univs
 
 let universes_of_global env r = 
     match r with
-    | VarRef id -> Univ.UContext.empty
+    | VarRef id -> Univ.AUContext.empty
     | ConstRef c -> 
       let cb = Environ.lookup_constant c env in 
-	Declareops.universes_of_polymorphic_constant
-          (Environ.opaque_tables env) cb
+      Declareops.constant_polymorphic_context cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
       Declareops.inductive_polymorphic_context mib
diff --git a/library/global.mli b/library/global.mli
index 754fa1516b..5ddf54b4af 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -141,7 +141,7 @@ val type_of_global_unsafe : Globnames.global_reference -> Constr.types
     [Evarutil.new_global] and [Retyping.get_type_of]. *)
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : Globnames.global_reference -> Univ.universe_context
+val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context
 
 (** {6 Retroknowledge } *)
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1cb694da66..9fc2573aca 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -198,7 +198,8 @@ let warn_projection_no_head_constant =
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
   let ctx = Environ.constant_context env con in
-  let u = Univ.UContext.instance ctx in
+  let u = Univ.AUContext.instance ctx in
+  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
@@ -298,7 +299,7 @@ let error_not_structure ref =
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
   let env = Global.env () in
-  let u = Environ.constant_instance env sp in
+  let u = Univ.AUContext.instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 201f79c39f..bae831b637 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') =
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-        Declareops.constant_polymorphic_instance cb
+        Univ.AUContext.instance (Declareops.constant_polymorphic_context cb)
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-         Declareops.inductive_polymorphic_instance mib
+         Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
       | _ -> Univ.Instance.empty
     in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
       Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b3eaa3cb95..66cc42cb61 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,7 +174,7 @@ and nf_whd env sigma whd typ =
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
      let mib = Environ.lookup_mind mi env in
      let nb_univs =
-       Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
+       Univ.AUContext.size (Declareops.inductive_polymorphic_context mib)
      in
      let mk u =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -203,7 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
   | ConstKey cst ->
      let cbody = Environ.lookup_constant cst env in
      let nb_univs =
-       Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
+       Univ.AUContext.size (Declareops.constant_polymorphic_context cbody)
      in
      let mk u =
        let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 15c0f80b93..d9bb97be10 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -78,6 +78,8 @@ let print_ref reduce ref =
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
+  let inst = Univ.AUContext.instance univs in
+  let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
   let bl = Universes.universe_binders_of_global ref in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
@@ -503,7 +505,10 @@ let ungeneralized_type_of_constant_type t =
 
 let print_instance sigma cb =
   if Declareops.constant_is_polymorphic cb then
-    pr_universe_instance sigma (Declareops.constant_polymorphic_context cb)
+    let univs = Declareops.constant_polymorphic_context cb in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    pr_universe_instance sigma univs
   else mt()
 				
 let print_constant with_values sep sp =
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 10b791e37f..2e0e6d2845 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -89,7 +89,7 @@ let build_ind_type env mip =
 
 let print_one_inductive env sigma mib ((_,i) as ind) =
   let u = if Declareops.inductive_is_polymorphic mib then 
-      Declareops.inductive_polymorphic_instance mib
+      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
@@ -100,7 +100,9 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
   let envpar = push_rel_context params env in
   let inst =
     if Declareops.inductive_is_polymorphic mib then
-      Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib)
+      let ctx = Declareops.inductive_polymorphic_context mib in
+      let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
+      Printer.pr_universe_instance sigma ctx
     else mt ()
   in
   hov 0 (
@@ -149,7 +151,7 @@ let get_fields =
 let print_record env mind mib =
   let u = 
     if Declareops.inductive_is_polymorphic mib then 
-      Declareops.inductive_polymorphic_instance mib
+      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
     else Univ.Instance.empty 
   in
   let mip = mib.mind_packets.(0) in
@@ -292,11 +294,13 @@ let print_body is_impl env mp (l,body) =
     | SFBmodule _ -> keyword "Module" ++ spc () ++ name
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
     | SFBconst cb ->
+       let ctx = Declareops.constant_polymorphic_context cb in
        let u =
 	 if Declareops.constant_is_polymorphic cb then
-            Declareops.constant_polymorphic_instance cb
+            Univ.AUContext.instance ctx
 	 else Univ.Instance.empty
        in
+       let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
        let sigma = Evd.empty in
       (match cb.const_body with
 	| Def _ -> def "Definition" ++ spc ()
@@ -316,8 +320,7 @@ let print_body is_impl env mp (l,body) =
 		       Printer.pr_lconstr_env env sigma
 			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx sigma 
-              (Declareops.constant_polymorphic_context cb))
+	    Printer.pr_universe_ctx sigma ctx)
     | SFBmind mib ->
       try
 	let env = Option.get env in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 5d9d36958f..e058806a35 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -48,7 +48,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
   else
     let mib,mip = Inductive.lookup_mind_specif env ind in
     let ctx = Declareops.inductive_polymorphic_context mib in
-    let u = Univ.UContext.instance ctx in
+    let u = Univ.AUContext.instance ctx in
+    let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
     let sigma = Evd.merge_universe_context sigma ectx in
@@ -62,7 +63,8 @@ let build_induction_scheme_in_type dep sort ind =
     let mib,mip = Inductive.lookup_mind_specif env ind in
       Declareops.inductive_polymorphic_context mib
   in
-  let u = Univ.UContext.instance ctx in
+  let u = Univ.AUContext.instance ctx in
+  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
   let ctxset = Univ.ContextSet.of_context ctx in
   let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in
   let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0acdaf57d..5a1c260b1f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -362,7 +362,7 @@ let get_body obl =
   match obl.obl_body with
   | None -> None
   | Some (DefinedObl c) ->
-    let u = Environ.constant_instance (Global.env ()) c in
+    let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in
     let pc = (c, u) in
       Some (DefinedObl pc)
   | Some (TermObl c) ->
diff --git a/vernac/record.ml b/vernac/record.ml
index d61f44cac8..366f504545 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,7 +265,7 @@ let warn_non_primitive_record =
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let u = Declareops.inductive_polymorphic_instance mib in
+  let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let poly = Declareops.inductive_is_polymorphic mib in
   let ctx =
@@ -547,7 +547,7 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
-    let inst = Declareops.inductive_polymorphic_instance mind in
+    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
diff --git a/vernac/search.ml b/vernac/search.ml
index 00536e52ec..788a2aa4a9 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let u = Declareops.inductive_polymorphic_instance mib in
+      let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
       let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
       let () = fn (IndRef ind) env typ in
-- 
cgit v1.2.3


From e1d4ad82b1557a8cf808e0374ece9c39ed349ea2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 23:33:42 +0200
Subject: Cleaning up the implementation of module subtyping in the kernel.

We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.

We also add a few tests for module subtyping in presence of polymorphic
constants.
---
 kernel/mod_typing.ml              | 27 +++++--------
 kernel/subtyping.mli              |  2 -
 kernel/uGraph.ml                  | 12 ++++++
 kernel/uGraph.mli                 |  4 ++
 kernel/univ.ml                    |  3 ++
 kernel/univ.mli                   |  6 ++-
 test-suite/modules/polymorphism.v | 81 +++++++++++++++++++++++++++++++++++++++
 7 files changed, 114 insertions(+), 21 deletions(-)
 create mode 100644 test-suite/modules/polymorphism.v

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 71c0370083..69fbd0f325 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -92,37 +92,28 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	         c, Reduction.infer_conv env' (Environ.universes env') c c'
 	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
         | Polymorphic_const uctx ->
-          let uctx = Univ.instantiate_univ_context uctx in
-	  let cus, ccst = Univ.UContext.dest uctx in
-	  let newus, cst = Univ.UContext.dest ctx in
-	  let () =
-	    if not (Univ.Instance.length cus == Univ.Instance.length newus) then
-	      error_incorrect_with_constraint lab
-	  in
-	  let inst = Univ.Instance.append cus newus in
-	  let csti = Univ.enforce_eq_instances cus newus cst in
-	  let csta = Univ.Constraint.union csti ccst in
-	  let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
-	  let () = if not (UGraph.check_constraints cst (Environ.universes env')) then
-		     error_incorrect_with_constraint lab
-	  in
+          let subst, ctx = Univ.abstract_universes ctx in
+          let c = Vars.subst_univs_level_constr subst c in
+          let () =
+            if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+              error_incorrect_with_constraint lab
+          in
+	  let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in
 	  let cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
 	      let typ = Typeops.type_of_constant_type env' cb.const_type in
-	      let typ = Vars.subst_instance_constr cus typ in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      cst'
 	    | Def cs ->
-	       let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in
+	       let c' = Mod_subst.force_constr cs in
 	       let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
 	        cst'
 	  in
 	    if not (Univ.Constraint.is_empty cst) then
 	      error_incorrect_with_constraint lab;
-	    let subst, ctx = Univ.abstract_universes ctx in
-	      Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty
+            c, Polymorphic_const ctx, Univ.ContextSet.empty
       in
       let def = Def (Mod_subst.from_val c') in
 (*      let ctx' = Univ.UContext.make (newus, cst) in *)
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index 6590d7e712..b24c20aa02 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -11,5 +11,3 @@ open Declarations
 open Environ
 
 val check_subtypes : env -> module_type_body -> module_type_body -> constraints
-
-
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 487257a776..9793dd881d 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -830,6 +830,18 @@ let sort_universes g =
   in
   normalize_universes g
 
+(** Subtyping of polymorphic contexts *)
+
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = UContext.dest (AUContext.repr ctx) in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs (Instance.to_array inst) in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
+
 (** Instances *)
 
 let check_eq_instances g t1 t2 =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 935a3cab4a..4de373eb4c 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -53,6 +53,10 @@ val check_constraints : constraints -> universes -> bool
 val check_eq_instances : Instance.t check_function
 (** Check equality of instances w.r.t. a universe graph *)
 
+val check_subtype : AUContext.t check_function
+(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
+    [ctx1]. *)
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
diff --git a/kernel/univ.ml b/kernel/univ.ml
index cb19761b32..6614d60276 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1060,6 +1060,9 @@ module AUContext =
 struct
   include UContext
 
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
   let instantiate inst (u, cst) =
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3d0d2234dc..9d93ec26cf 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -319,11 +319,15 @@ module AUContext :
 sig 
   type t
 
+  val repr : t -> UContext.t
+  (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of
+      the context and [cstr] the abstracted constraints. *)
+
   val empty : t
   val is_empty : t -> bool
 
   val instance : t -> Instance.t
-                        
+
   val size : t -> int
 
   (** Keeps the order of the instances *)
diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v
new file mode 100644
index 0000000000..63eaa382dc
--- /dev/null
+++ b/test-suite/modules/polymorphism.v
@@ -0,0 +1,81 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Parameter foo : Type@{i} -> Type@{j}.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := A.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive X@{i} : Type@{i} :=.
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Definition foo@{i} (A : Type@{i}) : Type@{i} := A.
+
+End KO_1.
+
+Fail Module KO_Test_1 : S := KO_1.
+
+(** Less general constraints *)
+
+Module KO_2.
+
+Section Foo.
+
+Universe i j.
+Constraint i < j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_2.
+
+Fail Module KO_Test_2 : S := KO_2.
+
+(** Less general constraints *)
+
+Module KO_3.
+
+Section Foo.
+
+Universe i j.
+Constraint i = j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.
-- 
cgit v1.2.3


From 40ec7bc85b78f68257593234016f82d8e78d6384 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 00:59:53 +0200
Subject: Properly handling polymorphic inductive subtyping in the kernel.

Before this patch, inductive subtyping was enforcing syntactic equality
of the variable instance, instead of reasoning up to alpha-renaming.
---
 kernel/modops.ml                   |   2 +-
 kernel/modops.mli                  |   2 +-
 kernel/subtyping.ml                | 104 ++++++++++++++-----------------------
 test-suite/modules/polymorphism2.v |  87 +++++++++++++++++++++++++++++++
 vernac/himsg.ml                    |   1 +
 5 files changed, 130 insertions(+), 66 deletions(-)
 create mode 100644 test-suite/modules/polymorphism2.v

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 24be46933e..a079bc8931 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -49,7 +49,7 @@ type signature_mismatch_error =
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.constraints
+  | IncompatibleConstraints of Univ.AUContext.t
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 4a150d54bd..e2a94b6919 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -108,7 +108,7 @@ type signature_mismatch_error =
   | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.constraints
+  | IncompatibleConstraints of Univ.AUContext.t
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6f128d5d30..bd82dd465b 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -80,10 +80,8 @@ let make_labmap mp list =
   List.fold_right add_one list empty_labmap
 
 
-let check_conv_error error why cst poly u f env a1 a2 =
+let check_conv_error error why cst poly f env a1 a2 =
   try 
-    let a1 = Vars.subst_instance_constr u a1 in
-    let a2 = Vars.subst_instance_constr u a2 in
     let cst' = f env (Environ.universes env) a1 a2 in
       if poly then 
 	if Constraint.is_empty cst' then cst
@@ -92,36 +90,42 @@ let check_conv_error error why cst poly u f env a1 a2 =
   with NotConvertible -> error why
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
+let check_polymorphic_instance error env auctx1 auctx2 =
+  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
+    error IncompatibleInstances
+  else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error (IncompatibleConstraints auctx1)
+  else
+    Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
   let kn1 = KerName.make2 mp1 l in
   let kn2 = KerName.make2 mp2 l in
   let error why = error_signature_mismatch l spec2 why in
-  let check_conv why cst poly u f = check_conv_error error why cst poly u f in
+  let check_conv why cst poly f = check_conv_error error why cst poly f in
   let mib1 =
     match info1 with
       | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib
       | _ -> error (InductiveFieldExpected mib2)
   in
-  let u =
-    let process inst inst' =
-      if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances
-    in
+  let env, inst =
     match mib1.mind_universes, mib2.mind_universes with
-    | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+    | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
     | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
-      process
-        (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | Cumulative_ind cumi, Cumulative_ind cumi' ->
-      process
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | _ -> error 
              (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2))
   in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
-  let check_inductive_type cst name env t1 t2 =
+  let check_inductive_type cst name t1 t2 =
 
     (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
@@ -154,7 +158,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	error (NotConvertibleInductiveField name)
       | _ -> (s1, s2) in
     check_conv (NotConvertibleInductiveField name)
-      cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+      cst (inductive_is_polymorphic mib1) infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
@@ -172,21 +176,20 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let ty1, cst1 = constrained_type_of_inductive env ((mib1,p1),u) in
-      let ty2, cst2 = constrained_type_of_inductive env ((mib2,p2),u) in
-      let cst = Constraint.union cst1 (Constraint.union cst2 cst) in
-      let cst = check_inductive_type cst p2.mind_typename env ty1 ty2 in
+      let ty1 = type_of_inductive env ((mib1, p1), inst) in
+      let ty2 = type_of_inductive env ((mib2, p2), inst) in
+      let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in
 	cst
   in
   let mind = mind_of_kn kn1 in
   let check_cons_types i cst p1 p2 =
     Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
-	(inductive_is_polymorphic mib1) u infer_conv env t1 t2)
+	(inductive_is_polymorphic mib1) infer_conv env t1 t2)
       cst
       p2.mind_consnames
-      (arities_of_specif (mind,u) (mib1,p1))
-      (arities_of_specif (mind,u) (mib2,p2))
+      (arities_of_specif (mind, inst) (mib1, p1))
+      (arities_of_specif (mind, inst) (mib2, p2))
   in
   let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
   check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
@@ -242,8 +245,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     
 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
   let error why = error_signature_mismatch l spec2 why in
-  let check_conv cst poly u f = check_conv_error error cst poly u f in
-  let check_type poly u cst env t1 t2 =
+  let check_conv cst poly f = check_conv_error error cst poly f in
+  let check_type poly cst env t1 t2 =
 
     let err = NotConvertibleTypeField (env, t1, t2) in
 
@@ -290,7 +293,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	  t1,t2
       else
         (t1,t2) in
-      check_conv err cst poly u infer_conv_leq env t1 t2
+      check_conv err cst poly infer_conv_leq env t1 t2
   in
   match info1 with
     | Constant cb1 ->
@@ -298,48 +301,21 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let cb1 = Declareops.subst_const_body subst1 cb1 in
       let cb2 = Declareops.subst_const_body subst2 cb2 in
       (* Start by checking universes *)
-      let poly = 
-	if not (Declareops.constant_is_polymorphic cb1 
-                 == Declareops.constant_is_polymorphic cb2) then
-           error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2))
-	else Declareops.constant_is_polymorphic cb2
-      in
-      let cst', env', u =
+      let poly, env =
         match cb1.const_universes, cb2.const_universes with
         | Monomorphic_const _, Monomorphic_const _ ->
-          cst, env, Univ.Instance.empty
+          false, env
         | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
-          begin
-	    let ctx1 = Univ.instantiate_univ_context auctx1 in
-	    let ctx2 = Univ.instantiate_univ_context auctx2 in
-	    let inst1, ctx1 = Univ.UContext.dest ctx1 in
-	    let inst2, ctx2 = Univ.UContext.dest ctx2 in
-	    if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then
-	      error IncompatibleInstances
-	    else 
-	      let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in
-	      let cstrs = Univ.Constraint.union cstrs ctx2 in
-	      try 
-		(* The environment with the expected universes plus equality 
-		   of the body instances with the expected instance *)
-		let ctxi = Univ.Instance.append inst1 inst2 in
-		let ctx = Univ.UContext.make (ctxi, cstrs) in
-		let env = Environ.push_context ctx env in
-		(* Check that the given definition does not add any constraint over
-		   the expected ones, so that it can be used in place of 
-                                 the original. *)
-		if UGraph.check_constraints ctx1 (Environ.universes env) then
-		  cstrs, env, inst2
-		else error (IncompatibleConstraints ctx1)
-	      with Univ.UniverseInconsistency incon -> 
-		error (IncompatibleUniverses incon)
-          end
-        | _ -> assert false
+          true, check_polymorphic_instance error env auctx1 auctx2
+        | Monomorphic_const _, Polymorphic_const _ ->
+          error (PolymorphicStatusExpected true)
+        | Polymorphic_const _, Monomorphic_const _ ->
+          error (PolymorphicStatusExpected false)
       in
       (* Now check types *)
-      let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
-      let typ2 = Typeops.type_of_constant_type env' cb2.const_type in
-      let cst = check_type poly u cst env' typ1 typ2 in
+      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let cst = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
 	   transparent constant.
@@ -356,7 +332,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		 Anyway [check_conv] will handle that afterwards. *)
 	      let c1 = Mod_subst.force_constr lc1 in
 	      let c2 = Mod_subst.force_constr lc2 in
-	      check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2))
+	      check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2))
    | IndType ((kn,i),mind1) ->
        CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v
new file mode 100644
index 0000000000..7e3327eee0
--- /dev/null
+++ b/test-suite/modules/polymorphism2.v
@@ -0,0 +1,87 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive foo@{i j} : Type@{i} -> Type@{j} :=.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Inductive foo@{i} : Type@{i} -> Type@{i} :=.
+
+End KO_1.
+
+Fail Module KO_Test_1 : S := KO_1.
+
+(** Less general constraints *)
+
+Module KO_2.
+
+Section Foo.
+
+Universe i j.
+Constraint i < j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End KO_2.
+
+Fail Module KO_Test_2 : S := KO_2.
+
+(** Less general constraints *)
+
+Module KO_3.
+
+Section Foo.
+
+Universe i j.
+Constraint i = j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ca3fb392fe..86dcb6d4dc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,6 +909,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
+      let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
-- 
cgit v1.2.3


From 8cd0413c0bd79256b59ffbbfd97d61af86f5cc25 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 14:31:52 +0200
Subject: Properly handling polymorphic inductive subtyping in the checker.

This is the followup of the previous commit, this time implementing the
correct algorithm in the checker.
---
 checker/subtyping.ml | 32 +++++++++++++++++++-------------
 checker/univ.ml      | 15 ++++++++++++++-
 checker/univ.mli     |  6 +++++-
 3 files changed, 38 insertions(+), 15 deletions(-)

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 303b18476d..3097c3a0b9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -81,6 +81,14 @@ let check_conv_error error f env a1 a2 =
   with
       NotConvertible -> error ()
 
+let check_polymorphic_instance error env auctx1 auctx2 =
+  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
+    error ()
+  else if not (Univ.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error ()
+  else
+    Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+
 (* for now we do not allow reorderings *)
 let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2= 
   let kn = MutInd.make2 mp1 l in
@@ -93,19 +101,17 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let mib2 = subst_mind subst2 mib2 in
   let check eq f = if not (eq (f mib1) (f mib2)) then error () in
-  let u =
-    let process inst inst' =
-      if Univ.Instance.equal inst inst' then inst else error ()
-    in
+  let env, u =
     match mib1.mind_universes, mib2.mind_universes with
-    | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+    | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
     | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
-      process
-        (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | Cumulative_ind cumi, Cumulative_ind cumi' ->
-      process
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | _ -> error ()
   in
   let eq_projection_body p1 p2 =
@@ -118,7 +124,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (eq_constr) (fun x -> snd x.proj_eta);
     check (eq_constr) (fun x -> x.proj_body); true
   in
-  let check_inductive_type env t1 t2 =
+  let check_inductive_type t1 t2 =
 
     (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
@@ -170,8 +176,8 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      check_inductive_type env
-        (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u))
+      check_inductive_type
+        (type_of_inductive env ((mib1,p1), u)) (type_of_inductive env ((mib2,p2),u))
   in
   let check_cons_types i p1 p2 =
     Array.iter2 (check_conv conv env)
diff --git a/checker/univ.ml b/checker/univ.ml
index 600af230c9..2cd4252b20 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1216,6 +1216,9 @@ module AUContext =
 struct
   include UContext
 
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
   let instantiate inst (u, cst) =
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
@@ -1278,7 +1281,17 @@ struct
 end
 type universe_context_set = ContextSet.t
 
-
+(** Instance subtyping *)
+
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = AUContext.repr ctx in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs inst in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
 
 (** Substitutions. *)
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 75c76cd129..01df46fa1e 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -212,6 +212,7 @@ sig
   val size : t -> int
 
   val instantiate : Instance.t -> t -> Constraint.t
+  val repr : t -> UContext.t
 
 end
 
@@ -289,7 +290,10 @@ val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_i
 
 (** Build the relative instance corresponding to the context *)
 val make_abstract_instance : abstract_universe_context -> universe_instance
-									    
+
+(** Check instance subtyping *)
+val check_subtype : universes -> AUContext.t -> AUContext.t -> bool
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.std_ppcmds
-- 
cgit v1.2.3


From c401fc96c3271746448600ca097876bd139b10e9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 15:26:44 +0200
Subject: Fix nonsensical universe abstraction in the kernel.

The function turning a side-effect declaration into the corresponding
entry was crazily wrong, as it used a named universe context quantifying
over DeBruijn universe indices. Declaring such entries resulted
in random anomalies.

This fixes bug #5641.
---
 kernel/term_typing.ml         | 2 +-
 test-suite/bugs/closed/5641.v | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/5641.v

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index eee227370e..3e516cae04 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -469,7 +469,7 @@ let constant_entry_of_side_effect cb u =
     match cb.const_universes with
     | Monomorphic_const ctx -> false, ctx
     | Polymorphic_const auctx -> 
-      true, Univ.instantiate_univ_context auctx
+      true, Univ.AUContext.repr auctx
   in
   let pt =
     match cb.const_body, u with
diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v
new file mode 100644
index 0000000000..9f3246f33d
--- /dev/null
+++ b/test-suite/bugs/closed/5641.v
@@ -0,0 +1,6 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j}.
+Proof.
+abstract (exact ltac:(abstract (exact A))).
+Defined.
-- 
cgit v1.2.3


From 91df402729f70144a4e4d198c4384dc515920e59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 15:42:43 +0200
Subject: Moving the last bits of abtraction-breaking code out of the kernel.

---
 API/API.mli           |  2 --
 kernel/declareops.ml  | 18 ------------------
 kernel/declareops.mli |  7 -------
 kernel/univ.mli       |  5 +++--
 library/global.ml     | 17 ++++++++++++++++-
 library/heads.ml      |  2 +-
 printing/prettyp.ml   | 11 ++++++++++-
 7 files changed, 30 insertions(+), 32 deletions(-)

diff --git a/API/API.mli b/API/API.mli
index 029f458cc7..9f7a6ded81 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4669,8 +4669,6 @@ sig
   val constant_has_body : Declarations.constant_body -> bool
   val is_opaque : Declarations.constant_body -> bool
   val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool
-  val body_of_constant :
-    Opaqueproof.opaquetab -> Declarations.constant_body -> Term.constr option
 end
 
 module Constr :
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index cf6d3c55e1..efce219826 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -44,29 +44,11 @@ let hcons_template_arity ar =
 
 (** {6 Constants } *)
 
-let instantiate cb c =
-  match cb.const_universes with
-  | Monomorphic_const _ -> c
-  | Polymorphic_const ctx -> 
-     Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
-
 let constant_is_polymorphic cb =
   match cb.const_universes with
   | Monomorphic_const _ -> false
   | Polymorphic_const _ -> true
 
-let body_of_constant otab cb = match cb.const_body with
-  | Undef _ -> None
-  | Def c -> Some (instantiate cb (force_constr c))
-  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
-
-let type_of_constant cb =
-  match cb.const_type with
-  | RegularArity t as x -> 
-    let t' = instantiate cb t in
-      if t' == t then x else RegularArity t'
-  | TemplateArity _ as x -> x
-
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
   | Def _ | OpaqueDef _ -> true
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 987c1adaf1..a8ba5fa392 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -32,13 +32,6 @@ val constant_polymorphic_context : constant_body -> abstract_universe_context
 (** Is the constant polymorphic? *)
 val constant_is_polymorphic : constant_body -> bool
 
-(** Accessing const_body, forcing access to opaque proof term if needed.
-    Only use this function if you know what you're doing. *)
-
-val body_of_constant :
-  Opaqueproof.opaquetab -> constant_body -> Term.constr option
-val type_of_constant : constant_body -> constant_type
-
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 9d93ec26cf..53297ac462 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -326,6 +326,7 @@ sig
   val empty : t
   val is_empty : t -> bool
 
+  (** Don't use. *)
   val instance : t -> Instance.t
 
   val size : t -> int
@@ -460,10 +461,10 @@ val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abs
 
 val make_abstract_instance : abstract_universe_context -> universe_instance
 
-(** Get the instantiated graph. *)
+(** Don't use. *)
 val instantiate_univ_context : abstract_universe_context -> universe_context
 
-(** Get the instantiated graphs for both universe constraints and subtyping constraints. *)
+(** Don't use. *)
 val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
 
 (** {6 Pretty-printing of universes. } *)
diff --git a/library/global.ml b/library/global.ml
index 09c202c500..e90151bffe 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -122,7 +122,22 @@ let lookup_modtype kn = lookup_modtype kn (env())
 let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
 let opaque_tables () = Environ.opaque_tables (env ())
-let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb
+
+let instantiate cb c =
+  let open Declarations in
+  match cb.const_universes with
+  | Monomorphic_const _ -> c
+  | Polymorphic_const ctx ->
+     Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
+
+let body_of_constant_body cb =
+  let open Declarations in
+  let otab = opaque_tables () in
+  match cb.const_body with
+  | Undef _ -> None
+  | Def c -> Some (instantiate cb (Mod_subst.force_constr c))
+  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
+
 let body_of_constant cst = body_of_constant_body (lookup_constant cst)
 
 (** Operations on kernel names *)
diff --git a/library/heads.ml b/library/heads.ml
index 0f420c0e65..a1cb812429 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -128,7 +128,7 @@ let compute_head = function
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
      if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
-     then Declareops.body_of_constant (Environ.opaque_tables env) cb else None 
+     then Global.body_of_constant cst else None
    in
      (match body with
      | None -> RigidHead (RigidParameter cst)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index d9bb97be10..ff12737f66 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -514,7 +514,16 @@ let print_instance sigma cb =
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
-  let typ = Declareops.type_of_constant cb in
+  let typ = match cb.const_type with
+  | RegularArity t as x ->
+    begin match cb.const_universes with
+    | Monomorphic_const _ -> x
+    | Polymorphic_const univs ->
+      let inst = Univ.AUContext.instance univs in
+      RegularArity (Vars.subst_instance_constr inst t)
+    end
+  | TemplateArity _ as x -> x
+  in
   let typ = ungeneralized_type_of_constant_type typ in
   let univs =
     let otab = Global.opaque_tables () in
-- 
cgit v1.2.3


From 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Jul 2017 11:44:53 +0200
Subject: Adding a comment regarding De Bruijn universe indices in the kernel.

---
 kernel/mod_typing.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 69fbd0f325..c7f3e5c51b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -98,6 +98,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
             if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
           in
+          (** Terms are compared in a context with De Bruijn universe indices *)
 	  let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in
 	  let cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
-- 
cgit v1.2.3