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/funind/glob_termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/glob_termops.ml')

diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 13ff19a46b..7b758da8e8 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function
 	mkGVar id
   | PatCstr(constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.constructor_nallargs_env
+        Inductiveops.constructor_nallargs
 	  (Global.env ())
 	  constr
       in
-- 
cgit v1.2.3