Remove calls to Global.env in Patternops

plugins/ltac/tacsubst.ml

@@ -99,7 +99,9 @@ let subst_evaluable subst =
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
 let subst_glob_constr_or_pattern subst (bvars,c,p) =
-  (bvars,subst_glob_constr subst c,subst_pattern (Global.env()) subst p)
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p)
 
 let subst_redexp subst =
   Redops.map_red_expr_gen

pretyping/patternops.ml

@@ -280,80 +280,78 @@ let rec liftn_pattern k n = function
 
 let lift_pattern k = liftn_pattern k 1
 
-let rec subst_pattern env subst pat =
+let rec subst_pattern env sigma subst pat =
   match pat with
   | PRef ref ->
     let ref',t = subst_global subst ref in
     if ref' == ref then pat else (match t with
         | None -> PRef ref'
         | Some t ->
-          let env = Global.env () in
-          let evd = Evd.from_env env in
-          pattern_of_constr env evd t.Univ.univ_abstracted_value)
+          pattern_of_constr env sigma t.Univ.univ_abstracted_value)
   | PVar _
   | PEvar _
   | PRel _
   | PInt _ -> pat
   | PProj (p,c) -> 
       let p' = Projection.map (subst_mind subst) p in
-      let c' = subst_pattern env subst c in
+      let c' = subst_pattern env sigma subst c in
 	if p' == p && c' == c then pat else
 	  PProj(p',c')
   | PApp (f,args) ->
-      let f' = subst_pattern env subst f in
-      let args' = Array.Smart.map (subst_pattern env subst) args in
+      let f' = subst_pattern env sigma subst f in
+      let args' = Array.Smart.map (subst_pattern env sigma subst) args in
 	if f' == f && args' == args then pat else
 	  PApp (f',args')
   | PSoApp (i,args) ->
-      let args' = List.Smart.map (subst_pattern env subst) args in
+      let args' = List.Smart.map (subst_pattern env sigma subst) args in
 	if args' == args then pat else
 	  PSoApp (i,args')
   | PLambda (name,c1,c2) ->
-      let c1' = subst_pattern env subst c1 in
-      let c2' = subst_pattern env subst c2 in
+      let c1' = subst_pattern env sigma subst c1 in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PLambda (name,c1',c2')
   | PProd (name,c1,c2) ->
-      let c1' = subst_pattern env subst c1 in
-      let c2' = subst_pattern env subst c2 in
+      let c1' = subst_pattern env sigma subst c1 in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PProd (name,c1',c2')
   | PLetIn (name,c1,t,c2) ->
-      let c1' = subst_pattern env subst c1 in
-      let t' = Option.Smart.map (subst_pattern env subst) t in
-      let c2' = subst_pattern env subst c2 in
+      let c1' = subst_pattern env sigma subst c1 in
+      let t' = Option.Smart.map (subst_pattern env sigma subst) t in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c1' == c1 && t' == t && c2' == c2 then pat else
 	  PLetIn (name,c1',t',c2')
   | PSort _
   | PMeta _ -> pat
   | PIf (c,c1,c2) ->
-      let c' = subst_pattern env subst c in
-      let c1' = subst_pattern env subst c1 in
-      let c2' = subst_pattern env subst c2 in
+      let c' = subst_pattern env sigma subst c in
+      let c1' = subst_pattern env sigma subst c1 in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c' == c && c1' == c1 && c2' == c2 then pat else
 	  PIf (c',c1',c2')
   | PCase (cip,typ,c,branches) ->
       let ind = cip.cip_ind in
       let ind' = Option.Smart.map (subst_ind subst) ind in
       let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
-      let typ' = subst_pattern env subst typ in
-      let c' = subst_pattern env subst c in
+      let typ' = subst_pattern env sigma subst typ in
+      let c' = subst_pattern env sigma subst c in
       let subst_branch ((i,n,c) as br) =
-        let c' = subst_pattern env subst c in
+        let c' = subst_pattern env sigma subst c in
 	if c' == c then br else (i,n,c')
       in
       let branches' = List.Smart.map subst_branch branches in
       if cip' == cip && typ' == typ && c' == c && branches' == branches
       then pat
       else PCase(cip', typ', c', branches')
   | PFix (lni,(lna,tl,bl)) ->
-      let tl' = Array.Smart.map (subst_pattern env subst) tl in
-      let bl' = Array.Smart.map (subst_pattern env subst) bl in
+      let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in
+      let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in
       if bl' == bl && tl' == tl then pat
       else PFix (lni,(lna,tl',bl'))
   | PCoFix (ln,(lna,tl,bl)) ->
-      let tl' = Array.Smart.map (subst_pattern env subst) tl in
-      let bl' = Array.Smart.map (subst_pattern env subst) bl in
+      let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in
+      let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in
       if bl' == bl && tl' == tl then pat
       else PCoFix (ln,(lna,tl',bl'))
 

pretyping/patternops.mli

@@ -21,7 +21,7 @@ val constr_pattern_eq : constr_pattern -> constr_pattern -> bool
 
 val occur_meta_pattern : constr_pattern -> bool
 
-val subst_pattern : Environ.env -> substitution -> constr_pattern -> constr_pattern
+val subst_pattern : Environ.env -> Evd.evar_map -> substitution -> constr_pattern -> constr_pattern
 
 val noccurn_pattern : int -> constr_pattern -> bool
 

tactics/hints.ml

@@ -1064,7 +1064,9 @@ let subst_autohint (subst, obj) =
   in
   let subst_hint (k,data as hint) =
     let k' = Option.Smart.map subst_key k in
-    let pat' = Option.Smart.map (subst_pattern (Global.env()) subst) data.pat in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
     let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->

tactics/redexpr.ml

@@ -259,10 +259,12 @@ let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
 
 let subst_red_expr subs =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   Redops.map_red_expr_gen
     (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
-    (Patternops.subst_pattern (Global.env()) subs)
+    (Patternops.subst_pattern env sigma subs)
 
 let inReduction : bool * string * red_expr -> obj =
   declare_object