Remove calls to Global.env in Glob_ops

interp/constrintern.ml

@@ -753,7 +753,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
           else
             let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
             match disjpat with
-            | [pat] -> (glob_constr_of_cases_pattern pat, None)
+            | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
             | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
         in
         let terms = Id.Map.fold mk_env terms Id.Map.empty in
@@ -815,7 +815,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       else
         let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
         match disjpat with
-        | [pat] -> glob_constr_of_cases_pattern pat
+        | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
         | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
     with Not_found ->
     try

interp/notation.ml

@@ -1516,7 +1516,7 @@ let uninterp_prim_token c =
      with Not_found -> raise Notation_ops.No_match
 
 let uninterp_prim_token_cases_pattern c =
-  match glob_constr_of_closed_cases_pattern c with
+  match glob_constr_of_closed_cases_pattern (Global.env()) c with
   | exception Not_found -> raise Notation_ops.No_match
   | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
 

interp/notation_ops.ml

@@ -1292,7 +1292,7 @@ let match_notation_constr u c (metas,pat) =
     | NtnTypeBinder (NtnBinderParsedAsConstr _) ->
        (match Id.List.assoc x binders with
         | [pat] ->
-          let v = glob_constr_of_cases_pattern pat in
+          let v = glob_constr_of_cases_pattern (Global.env()) pat in
           ((v,scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
     | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
@@ -1333,11 +1333,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
   | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
-      let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
+      let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
       sigma,(0,l)
   | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
-      let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
+      let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
       then

pretyping/glob_ops.ml

@@ -539,8 +539,8 @@ let drop_local_defs params decls args =
       | _ -> assert false in
     aux decls args
 
-let add_patterns_for_params_remove_local_defs (ind,j) l =
-  let (mib,mip) = Global.lookup_inductive ind in
+let add_patterns_for_params_remove_local_defs env (ind,j) l =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let nparams = mib.Declarations.mind_nparams in
   let l =
     if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
@@ -556,12 +556,12 @@ let add_alias ?loc na c =
   | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
 
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function
+let rec glob_constr_of_cases_pattern_aux env isclosed x = DAst.map_with_loc (fun ?loc -> function
   | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None))
   | PatCstr (cstr,l,na)  ->
       let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
-      let l = add_patterns_for_params_remove_local_defs cstr l in
-      add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l))
+      let l = add_patterns_for_params_remove_local_defs env cstr l in
+      add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux env isclosed) l))
   | PatVar (Name id) when not isclosed ->
       GVar id
   | PatVar Anonymous when not isclosed ->
@@ -571,14 +571,14 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo
   | _ -> raise Not_found
   ) x
 
-let glob_constr_of_closed_cases_pattern p = match DAst.get p with
+let glob_constr_of_closed_cases_pattern env p = match DAst.get p with
   | PatCstr (cstr,l,na) ->
       let loc = p.CAst.loc in
-      na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
+      na,glob_constr_of_cases_pattern_aux env true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
 
-let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
+let glob_constr_of_cases_pattern env p = glob_constr_of_cases_pattern_aux env false p
 
 (* This has to be in some file... *)
 

pretyping/glob_ops.mli

@@ -96,12 +96,13 @@ val map_pattern : (glob_constr -> glob_constr) ->
     @raise Not_found if translation is impossible *)
 val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
 
-val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g
+val glob_constr_of_closed_cases_pattern : Environ.env -> 'a cases_pattern_g -> Name.t * 'a glob_constr_g
 
 (** A canonical encoding of cases pattern into constr such that
     composed with [cases_pattern_of_glob_constr Anonymous] gives identity *)
-val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
+val glob_constr_of_cases_pattern : Environ.env -> 'a cases_pattern_g -> 'a glob_constr_g
 
-val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
+val add_patterns_for_params_remove_local_defs : Environ.env -> constructor ->
+  'a cases_pattern_g list -> 'a cases_pattern_g list
 
 val empty_lvar : Ltac_pretype.ltac_var_map