From 316592a31b463568f5136757c3570eaa8e1f0167 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 25 Sep 2020 15:31:51 +0200
Subject: Put type-in-type flag in ugraph.

Fix #13086.
---
 engine/uState.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index 8d1584cd95..2cb88c7fff 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -286,6 +286,10 @@ let process_universe_constraints ctx cstrs =
             if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local
           | UEq (l, r) -> equalize_universes l r local
   in
+  let unify_universes cst local =
+    if not (UGraph.type_in_type univs) then unify_universes cst local
+    else try unify_universes cst local with UniverseInconsistency _ -> local
+  in
   let local =
     UnivProblem.Set.fold unify_universes cstrs Constraint.empty
   in
-- 
cgit v1.2.3