From 4585baa53e7fa4c25e304b8136944748a7622e10 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 18:42:38 +0200
Subject: Univs: refined handling of assumptions

According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
---
 library/lib.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 81db547efd..f4f52db53b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -420,6 +420,7 @@ let extract_hyps (secs,ohyps) =
   in aux (secs,ohyps)
 
 let instance_from_variable_context sign =
+
   let rec inst_rec = function
     | (id,b,None,_) :: sign -> id :: inst_rec sign
     | _ :: sign -> inst_rec sign
-- 
cgit v1.2.3