From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 26 Apr 2017 15:24:35 +0200
Subject: Fix bugs

---
 library/declare.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index fcaadaa6e0..bf5313545c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -364,9 +364,9 @@ let infer_inductive_subtyping (pth, mind_ent) =
       let env' =
         Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env
       in
-      let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in
-      let evd = Evd.from_env env'' in
-        (pth, Inductiveops.infer_inductive_subtyping env'' evd mind_ent)
+      (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
+      let evd = Evd.from_env env' in
+        (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
     end
   else (pth, mind_ent)
 
-- 
cgit v1.2.3