From 8361be1d785f8588d2d3c2a0df7a1d9239bae5a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 Oct 2018 16:45:34 +0200
Subject: Remove a few circumvolutions around parameters of inductive entries

---
 pretyping/inferCumulativity.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index a56a8314e6..422a05c19a 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -196,7 +196,7 @@ let infer_inductive env mie =
         Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
           LMap.empty uarray
       in
-      let env, _ = Typeops.infer_local_decls env params in
+      let env = Typeops.check_context env params in
       let variances = List.fold_left (fun variances entry ->
           let variances = infer_arity_constructor true
               env variances entry.mind_entry_arity
-- 
cgit v1.2.3