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.

17 files changed, 45 insertions, 109 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 93ffa329a..a145165aa 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 698b8b77c..b8cbda7cf 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 93b8b907c..0b605820d 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 5fd5510a7..303b18476 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 b434db129..4eebcb25b 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 457ccbdff..faa682cbf 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 28058aeed..5df02c8a9 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 b9e7ec169..852f87d5e 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 04971f83d..e248436ec 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 1acede729..9d7262206 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 de4efbba9..423e0d934 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 283febed2..eee227370 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 009eb88fc..439f83578 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 669be2d45..3bafb824d 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 b5f7715b1..09147cb41 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 b5d195873..2acf6bfe6 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 cc1709f1c..3acefa134 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 =