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

---
 vernac/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/command.ml')

diff --git a/vernac/command.ml b/vernac/command.ml
index 116a7aee16..6c59976232 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -662,7 +662,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     }
   in
   (if poly then
-      Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent
+      Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
    else mind_ent), pl, impls
 
 (* Very syntactical equality *)
-- 
cgit v1.2.3