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.
---
 kernel/term_typing.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'kernel/term_typing.ml')

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