Remove one call to Global.env in Detyping

One other call still remains, but will require to refactor some
section-handling code.

1 files changed, 22 insertions, 22 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 4e3c77cb1a..9ce63e4207 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -280,7 +280,7 @@ let rec liftn_pattern k n = function
 
 let lift_pattern k = liftn_pattern k 1
 
-let rec subst_pattern subst pat =
+let rec subst_pattern env subst pat =
   match pat with
   | PRef ref ->
     let ref',t = subst_global subst ref in
@@ -296,50 +296,50 @@ let rec subst_pattern subst pat =
   | PInt _ -> pat
   | PProj (p,c) -> 
       let p' = Projection.map (subst_mind subst) p in
-      let c' = subst_pattern subst c in
+      let c' = subst_pattern env subst c in
 	if p' == p && c' == c then pat else
 	  PProj(p',c')
   | PApp (f,args) ->
-      let f' = subst_pattern subst f in
-      let args' = Array.Smart.map (subst_pattern subst) args in
+      let f' = subst_pattern env subst f in
+      let args' = Array.Smart.map (subst_pattern env subst) args in
 	if f' == f && args' == args then pat else
 	  PApp (f',args')
   | PSoApp (i,args) ->
-      let args' = List.Smart.map (subst_pattern subst) args in
+      let args' = List.Smart.map (subst_pattern env subst) args in
 	if args' == args then pat else
 	  PSoApp (i,args')
   | PLambda (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
+      let c1' = subst_pattern env subst c1 in
+      let c2' = subst_pattern env subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PLambda (name,c1',c2')
   | PProd (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
+      let c1' = subst_pattern env subst c1 in
+      let c2' = subst_pattern env subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PProd (name,c1',c2')
   | PLetIn (name,c1,t,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let t' = Option.Smart.map (subst_pattern subst) t in
-      let c2' = subst_pattern subst c2 in
+      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
 	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 subst c in
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
+      let c' = subst_pattern env subst c in
+      let c1' = subst_pattern env subst c1 in
+      let c2' = subst_pattern env 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 subst typ in
-      let c' = subst_pattern subst c in
+      let typ' = subst_pattern env subst typ in
+      let c' = subst_pattern env subst c in
       let subst_branch ((i,n,c) as br) =
-	let c' = subst_pattern subst c in
+        let c' = subst_pattern env subst c in
 	if c' == c then br else (i,n,c')
       in
       let branches' = List.Smart.map subst_branch branches in
@@ -347,13 +347,13 @@ let rec subst_pattern subst pat =
       then pat
       else PCase(cip', typ', c', branches')
   | PFix (lni,(lna,tl,bl)) ->
-      let tl' = Array.Smart.map (subst_pattern subst) tl in
-      let bl' = Array.Smart.map (subst_pattern subst) bl in
+      let tl' = Array.Smart.map (subst_pattern env subst) tl in
+      let bl' = Array.Smart.map (subst_pattern env 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 subst) tl in
-      let bl' = Array.Smart.map (subst_pattern subst) bl in
+      let tl' = Array.Smart.map (subst_pattern env subst) tl in
+      let bl' = Array.Smart.map (subst_pattern env subst) bl in
       if bl' == bl && tl' == tl then pat
       else PCoFix (ln,(lna,tl',bl'))