From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 engine/univProblem.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/univProblem.ml')

diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 08ff9efa5b..8d6689933c 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -150,7 +150,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
   let cstrs = ref accu in
-  let eq_universes _ _ = UGraph.check_eq_instances univs in
+  let eq_universes _ = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 =
     if Sorts.equal s1 s2 then true
     else
-- 
cgit v1.2.3