From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 15 Jun 2017 16:50:05 +0200
Subject: Fix a bug in cumulativity

---
 pretyping/evarconv.ml      | 9 +++++----
 pretyping/reductionops.mli | 1 -
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b15dde5d79..d84363089d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,12 +353,13 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 let check_leq_inductives evd cumi u u' =
   let u = EConstr.EInstance.kind evd u in
   let u' = EConstr.EInstance.kind evd u' in
-  let ind_instance = 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) 
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
   in
   let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     begin
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index af4ea3ac53..a4da19de75 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -66,7 +66,6 @@ module Cst_stack : sig
   val pr : t -> Pp.std_ppcmds
 end
 
-
 module Stack : sig
   type 'a app_node
 
-- 
cgit v1.2.3