From 5af486406e366bf23558311a7367e573c617e078 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 Apr 2019 12:18:49 +0200
Subject: Remove calls to global env in Inductiveops

---
 plugins/firstorder/sequent.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder/sequent.ml')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 01b18e2f30..9f2ceb2c28 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -188,7 +188,7 @@ let empty_seq depth=
 let expand_constructor_hints =
   List.map_append (function
     | GlobRef.IndRef ind ->
-        List.init (Inductiveops.nconstructors ind)
+        List.init (Inductiveops.nconstructors (Global.env()) ind)
           (fun i -> GlobRef.ConstructRef (ind,i+1))
     | gr ->
 	[gr])
-- 
cgit v1.2.3