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/formula.ml | 8 ++++----
 plugins/firstorder/sequent.ml | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 56b3dc97cf..4b7bc707d6 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -82,13 +82,13 @@ let pop t = Vars.lift (-1) t
 let kind_of_formula env sigma term =
   let normalize = special_nf env sigma in
   let cciterm = special_whd env sigma term in
-    match match_with_imp_term sigma cciterm with
+    match match_with_imp_term env sigma cciterm with
 	Some (a,b)-> Arrow (a, pop b)
       |_->
-	 match match_with_forall_term sigma cciterm with
+         match match_with_forall_term env sigma cciterm with
 	     Some (_,a,b)-> Forall (a, b)
 	   |_->
-	      match match_with_nodep_ind sigma cciterm with
+              match match_with_nodep_ind env sigma cciterm with
 		  Some (i,l,n)->
 		    let ind,u=EConstr.destInd sigma i in
 		    let u = EConstr.EInstance.kind sigma u in
@@ -111,7 +111,7 @@ let kind_of_formula env sigma term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type sigma cciterm with
+                    match match_with_sigma_type env sigma cciterm with
 			Some (i,l)->
                           let (ind, u) = EConstr.destInd sigma i in
                           let u = EConstr.EInstance.kind sigma u in
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