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.
---
 engine/universes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine')

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