From 90dfacaacfec8265b11dc9291de9510f515c0081 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Oct 2015 23:59:05 +0100
Subject: Conversion of polymorphic inductive types was incomplete in VM and
 native.

Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
---
 pretyping/reductionops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bb1bc7d2ea..0714c93b4f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1282,7 +1282,7 @@ let sigma_compare_sorts env pb s0 s1 sigma =
   | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
     
-let sigma_compare_instances flex i0 i1 sigma =
+let sigma_compare_instances ~flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
   with Evd.UniversesDiffer
      | Univ.UniverseInconsistency _ ->
-- 
cgit v1.2.3