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

---
 kernel/indtypes.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b976469ff7..0346026aa4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -271,7 +271,8 @@ let typecheck_inductive env mie =
     | Polymorphic_ind_entry ctx -> push_context ctx env
     | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
-  let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
+  let env_params = check_context env' mie.mind_entry_params in
+  let paramsctxt = mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
   (* the set of constraints *)
-- 
cgit v1.2.3