Fix a bug in cumulativity

8 files changed, 23 insertions, 20 deletions

diff --git a/dev/base_include b/dev/base_include
index f9af0696b..8ee1cceb2 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -58,8 +58,6 @@
 
 (* Open main files *)
 
-open API
-open Grammar_API
 open Names
 open Term
 open Vars
diff --git a/dev/include b/dev/include
index 1d87456de..31ae5da71 100644
--- a/dev/include
+++ b/dev/include
@@ -41,7 +41,8 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* univ info *) ppcumulativity_info;;
+#install_printer  (* cumulativity info *) ppcumulativity_info;;
+#install_printer  (* abstract cumulativity info *) ppabstract_cumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index abf6db1b7..ff575e432 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,7 +8,6 @@
 
 (* Printers for the ocaml toplevel. *)
 
-open API
 open Util
 open Pp
 open Names
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index be6b914b6..afa94a63e 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,4 +1,3 @@
-open API
 open Format
 open Term
 open Names
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a9e2ce78c..605e9f314 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -679,12 +679,13 @@ let infer_check_conv_constructors
       infer_check_inductive_instances CONV cumi u1 u2 univs
 
 let check_inductive_instances cv_pb cumi u u' univs =
-  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_subtypctx = 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
     let comp_cst =
@@ -765,13 +766,14 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
   in (univs, cstrs')
 
 let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
-  let ind_instance = 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi) 
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
   in
   let ind_subtypctx =  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
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  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
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b15dde5d7..d84363089 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 af4ea3ac5..a4da19de7 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
 
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index ecf9035bf..ebf817cfc 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -58,4 +58,8 @@ Section subtyping_test.
 
   Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
 
-End subtyping_test.
\ No newline at end of file
+End subtyping_test.
+
+Record A : Type := { a :> Type; }.
+
+Record B (X : A) : Type := { b : X; }.
\ No newline at end of file