From 0d9a91113c4112eece0680e433f435fdfb39ea4b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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.
---
 library/lib.ml      |  3 ++-
 library/univops.ml  | 39 ---------------------------------------
 library/univops.mli |  2 --
 3 files changed, 2 insertions(+), 42 deletions(-)

(limited to 'library')

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
-- 
cgit v1.2.3