Remove calls to global env in Inductiveops

interp/constrextern.ml

@@ -212,7 +212,7 @@ let encode_record r =
 
 module PrintingRecordRecord =
   PrintingInductiveMake (struct
-    let encode = encode_record
+    let encode _env = encode_record
     let field = "Record"
     let title = "Types leading to pretty-printing using record notation: "
     let member_message s b =
@@ -224,7 +224,7 @@ module PrintingRecordRecord =
 
 module PrintingRecordConstructor =
   PrintingInductiveMake (struct
-    let encode = encode_record
+    let encode _env = encode_record
     let field = "Constructor"
     let title = "Types leading to pretty-printing using constructor form: "
     let member_message s b =
@@ -289,11 +289,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l
 
 let add_patt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l
+    Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l
 
 let add_cpatt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn  (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l
+    Util.List.addn  (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -364,7 +364,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
-  let nb_params = Inductiveops.inductive_nparams ind in
+  let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in
   List.exists (fun (_,impls) ->
     (List.length impls >= nb_params) &&
       let params,args = Util.List.chop nb_params impls in
@@ -526,7 +526,7 @@ let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = functi
 let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
-  if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
+  if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then
     let c = extern_reference vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
     CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])

interp/constrintern.ml

@@ -658,7 +658,7 @@ let terms_of_binders bl =
     | PatCstr (c,l,_) ->
        let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
-       let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
+       let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
        CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables l = match l with
     | bnd :: l ->
@@ -1212,10 +1212,10 @@ let check_or_pat_variables loc ids idsl =
     @return if letin are included *)
 let check_constructor_length env loc cstr len_pl pl0 =
   let n = len_pl + List.length pl0 in
-  if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
-    (Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
+  if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else
+    (Int.equal n (Inductiveops.constructor_nalldecls env cstr) ||
       (error_wrong_numarg_constructor ?loc env cstr
-         (Inductiveops.constructor_nrealargs cstr)))
+         (Inductiveops.constructor_nrealargs env cstr)))
 
 open Declarations
 
@@ -1241,9 +1241,9 @@ let add_local_defs_and_check_length loc env g pl args = match g with
         have been given in the "explicit" arguments, which come from a
         "@C args" notation or from a custom user notation *)
      let pl' = insert_local_defs_in_pattern cstr pl in
-     let maxargs = Inductiveops.constructor_nalldecls cstr in
+     let maxargs = Inductiveops.constructor_nalldecls env cstr in
      if List.length pl' + List.length args > maxargs then
-       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr);
+       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
      (* Two possibilities: either the args are given with explict
      variables for local definitions, then we give the explicit args
      extended with local defs, so that there is nothing more to be
@@ -1273,24 +1273,24 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
   in aux 0 (impl_list,pl2)
 
 let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
-  let nargs = Inductiveops.constructor_nallargs c in
-  let nargs' = Inductiveops.constructor_nalldecls c in
+  let nargs = Inductiveops.constructor_nallargs env c in
+  let nargs' = Inductiveops.constructor_nalldecls env c in
   let impls_st = implicits_of_global (ConstructRef c) in
   add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
     nargs nargs' impls_st len_pl1 pl2
 
 let add_implicits_check_ind_length env loc c len_pl1 pl2 =
-  let nallargs = inductive_nallargs_env env c in
-  let nalldecls = inductive_nalldecls_env env c in
+  let nallargs = inductive_nallargs env c in
+  let nalldecls = inductive_nalldecls env c in
   let impls_st = implicits_of_global (IndRef c) in
   add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
     nallargs nalldecls impls_st len_pl1 pl2
 
 (** Do not raise NotEnoughArguments thanks to preconditions*)
 let chop_params_pattern loc ind args with_letin =
   let nparams = if with_letin
-    then Inductiveops.inductive_nparamdecls ind
-    else Inductiveops.inductive_nparams ind in
+    then Inductiveops.inductive_nparamdecls (Global.env()) ind
+    else Inductiveops.inductive_nparams (Global.env()) ind in
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
   List.iter (fun c -> match DAst.get c with
@@ -1310,10 +1310,11 @@ let find_constructor loc add_params ref =
   in
   cstr, match add_params with
     | Some nb_args ->
+      let env = Global.env () in
       let nb =
-        if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr)
-          then Inductiveops.inductive_nparamdecls ind
-          else Inductiveops.inductive_nparams ind
+        if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr)
+        then Inductiveops.inductive_nparamdecls env ind
+        else Inductiveops.inductive_nparams env ind
       in
       List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
     | None -> []

interp/notation_ops.ml

@@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function
   | GApp (t, l) ->
     begin match DAst.get t with
     | GRef (ConstructRef cstr,_) ->
-     let nparams = Inductiveops.inductive_nparams (fst cstr) in
+     let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in
      let _,l = List.chop nparams l in
      PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
     | _ -> raise No_match
@@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
 let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
-  let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
+  let env = Global.env () in
+  let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in
   try
     (* If already bound to a binder, unify the term and the binder *)
     let patl' = Id.List.assoc var binders in

library/goptions.ml

@@ -57,7 +57,7 @@ module MakeTable =
 	  type key
 	  val compare : t -> t -> int
 	  val table : (string * key table_of_A) list ref
-	  val encode : key -> t
+          val encode : Environ.env -> key -> t
 	  val subst : substitution -> t -> t
           val printer : t -> Pp.t
           val key : option_name
@@ -111,10 +111,10 @@ module MakeTable =
 
     class table_of_A () =
     object
-      method add x = add_option (A.encode x)
-      method remove x = remove_option (A.encode x)
+      method add x = add_option (A.encode (Global.env()) x)
+      method remove x = remove_option (A.encode (Global.env()) x)
       method mem x =
-	let y = A.encode x in
+        let y = A.encode (Global.env()) x in
         let answer = MySet.mem y !t in
         Feedback.msg_info (A.member_message y answer)
       method print = print_table A.title A.printer !t
@@ -142,7 +142,7 @@ struct
   type key = string
   let compare = String.compare
   let table = string_table
-  let encode x = x
+  let encode _env x = x
   let subst _ x = x
   let printer = str
   let key = A.key
@@ -161,7 +161,7 @@ module type RefConvertArg =
 sig
   type t
   val compare : t -> t -> int
-  val encode : qualid -> t
+  val encode : Environ.env -> qualid -> t
   val subst : substitution -> t -> t
   val printer : t -> Pp.t
   val key : option_name

library/goptions.mli

@@ -89,8 +89,8 @@ module MakeRefTable :
     (A : sig
            type t
            val compare : t -> t -> int
-           val encode : qualid -> t
-	   val subst : substitution -> t -> t
+           val encode : Environ.env -> qualid -> t
+           val subst : substitution -> t -> t
            val printer : t -> Pp.t
            val key : option_name
            val title : string

plugins/cc/cctac.ml

@@ -67,7 +67,7 @@ let rec decompose_term env sigma t=
 	let canon_mind = MutInd.make1 (MutInd.canonical mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
-	let nargs=constructor_nallargs_env env (canon_ind,i_con) in
+        let nargs=constructor_nallargs env (canon_ind,i_con) in
 	  Constructor {ci_constr= ((canon_ind,i_con),u);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}

plugins/extraction/extraction.ml

@@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
 and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = constructors_nrealargs_env env ip in
+  let ni = constructors_nrealargs env ip in
   let br_size = Array.length br in
   assert (Int.equal (Array.length ni) br_size);
   if Int.equal br_size 0 then begin

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

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])

plugins/funind/glob_term_to_relation.ml

@@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl =
 		  Impargs.implicits_of_global constructref
 		in
 		let cst_narg =
-		  Inductiveops.constructor_nallargs_env
+                  Inductiveops.constructor_nallargs
 		    (Global.env ())
 		    construct
 		in
@@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl =
 		let pat_as_term =
 		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
 		in
-		cases_pattern_of_glob_constr Anonymous pat_as_term
+                cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
 	     )
     ind.Declarations.mind_consnames
 
@@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
 	mkGVar id
   | PatCstr(constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.constructor_nallargs_env
+        Inductiveops.constructor_nallargs
 	  (Global.env ())
 	  constr
       in

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

plugins/ltac/tauto.ml

@@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
 (** Test *)
 
 let is_empty _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
-  if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail
+  if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail
 
 (* Strictly speaking, this exceeds the propositional fragment as it
    matches also equality types (and solves them if a reflexivity) *)
 let is_unit_or_eq _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
-  if test sigma (assoc_var "X1" ist) then idtac else fail
+  if test genv sigma (assoc_var "X1" ist) then idtac else fail
 
 let bugged_is_binary sigma t =
   isApp sigma t &&
@@ -121,23 +123,25 @@ let bugged_is_binary sigma t =
 (** Dealing with conjunction *)
 
 let is_conj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let ind = assoc_var "X1" ist in
     if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) &&
-       is_conjunction sigma
+       is_conjunction genv sigma
          ~strict:flags.strict_in_hyp_and_ccl
          ~onlybinary:flags.binary_mode ind
     then idtac
     else fail
 
 let flatten_contravariant_conj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_conjunction sigma
+  match match_with_conjunction genv sigma
           ~strict:flags.strict_in_contravariant_hyp
           ~onlybinary:flags.binary_mode typ
   with
@@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist =
 (** Dealing with disjunction *)
 
 let is_disj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let t = assoc_var "X1" ist in
   if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) &&
-     is_disjunction sigma
+     is_disjunction genv sigma
        ~strict:flags.strict_in_hyp_and_ccl
        ~onlybinary:flags.binary_mode t
   then idtac
   else fail
 
 let flatten_contravariant_disj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_disjunction sigma
+  match match_with_disjunction genv sigma
           ~strict:flags.strict_in_contravariant_hyp
           ~onlybinary:flags.binary_mode
           typ with

plugins/ssr/ssrequality.ml

@@ -504,9 +504,9 @@ let rwprocess_rule dir rule gl =
          let sigma, rs2 = loop d sigma s a.(1) rs 0 in
          let s, sigma = sr sigma 1 in
          loop d sigma s a.(0) rs2 0
-      | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None ->
+      | App (r_eq, a) when Hipattern.match_with_equality_type env sigma t != None ->
         let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in
-        let np = Inductiveops.inductive_nparamdecls ind in
+        let np = Inductiveops.inductive_nparamdecls env ind in
         let indu = (ind, EConstr.EInstance.kind sigma u) in
         let ind_ct = Inductiveops.type_of_constructors env indu in
         let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in