From 2db70092d63065be8a5902764e0d1d5f1ea01e6c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Mon, 20 Nov 2017 18:43:31 +0100
Subject: Fix universe polymorphic Program obligations.

The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
---
 engine/uState.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index dfea25dd0..01a479821 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -437,6 +437,9 @@ let make_flexible_variable ctx ~algebraic u =
   {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}
 
+let make_flexible_nonalgebraic ctx =
+  {ctx with uctx_univ_algebraic = Univ.LSet.empty}
+
 let is_sort_variable uctx s = 
   match s with 
   | Sorts.Type u -> 
-- 
cgit v1.2.3