From 441bea723c511ed9e18ef005678bd01242b45c49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 13 Dec 2017 13:57:10 +0100
Subject: Returning instance instead of substitution in universe context
 abstraction.

This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
---
 kernel/univ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8cf9028fb..fee431ff4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1168,7 +1168,7 @@ let abstract_universes ctx =
       (UContext.constraints ctx)
   in
   let ctx = UContext.make (instance, cstrs) in
-  subst, ctx
+  instance, ctx
 
 let abstract_cumulativity_info (univcst, substcst) = 
   let instance, univcst = abstract_universes univcst in
-- 
cgit v1.2.3