Remove one call to Global.env in Detyping

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

4 files changed, 48 insertions, 49 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 87d3880f99..5003d0eec6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1014,13 +1014,12 @@ let rec subst_cases_pattern subst = DAst.map (function
 
 let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
-let rec subst_glob_constr subst = DAst.map (function
+let rec subst_glob_constr env subst = DAst.map (function
   | GRef (ref,u) as raw ->
     let ref',t = subst_global subst ref in
     if ref' == ref then raw else (match t with
         | None -> GRef (ref', u)
         | Some t ->
-          let env = Global.env () in
           let evd = Evd.from_env env in
           let t = t.Univ.univ_abstracted_value in (* XXX This seems dangerous *)
           DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)))
@@ -1032,33 +1031,33 @@ let rec subst_glob_constr subst = DAst.map (function
   | GPatVar _ as raw -> raw
 
   | GApp (r,rl) as raw ->
-      let r' = subst_glob_constr subst r
-      and rl' = List.Smart.map (subst_glob_constr subst) rl in
+      let r' = subst_glob_constr env subst r
+      and rl' = List.Smart.map (subst_glob_constr env subst) rl in
 	if r' == r && rl' == rl then raw else
 	  GApp(r',rl')
 
   | GLambda (n,bk,r1,r2) as raw ->
-      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
+      let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  GLambda (n,bk,r1',r2')
 
   | GProd (n,bk,r1,r2) as raw ->
-      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
+      let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  GProd (n,bk,r1',r2')
 
   | GLetIn (n,r1,t,r2) as raw ->
-      let r1' = subst_glob_constr subst r1 in
-      let r2' = subst_glob_constr subst r2 in
-      let t' = Option.Smart.map (subst_glob_constr subst) t in
+      let r1' = subst_glob_constr env subst r1 in
+      let r2' = subst_glob_constr env subst r2 in
+      let t' = Option.Smart.map (subst_glob_constr env subst) t in
 	if r1' == r1 && t == t' && r2' == r2 then raw else
 	  GLetIn (n,r1',t',r2')
 
   | GCases (sty,rtno,rl,branches) as raw ->
     let open CAst in
-      let rtno' = Option.Smart.map (subst_glob_constr subst) rtno
+      let rtno' = Option.Smart.map (subst_glob_constr env subst) rtno
       and rl' = List.Smart.map (fun (a,x as y) ->
-        let a' = subst_glob_constr subst a in
+        let a' = subst_glob_constr env subst a in
         let (n,topt) = x in
         let topt' = Option.Smart.map
           (fun ({loc;v=((sp,i),y)} as t) ->
@@ -1069,7 +1068,7 @@ let rec subst_glob_constr subst = DAst.map (function
                         (fun ({loc;v=(idl,cpl,r)} as branch) ->
 			   let cpl' =
                              List.Smart.map (subst_cases_pattern subst) cpl
-			   and r' = subst_glob_constr subst r in
+                           and r' = subst_glob_constr env subst r in
 			     if cpl' == cpl && r' == r then branch else
                                CAst.(make ?loc (idl,cpl',r')))
 			branches
@@ -1078,27 +1077,27 @@ let rec subst_glob_constr subst = DAst.map (function
 	  GCases (sty,rtno',rl',branches')
 
   | GLetTuple (nal,(na,po),b,c) as raw ->
-      let po' = Option.Smart.map (subst_glob_constr subst) po
-      and b' = subst_glob_constr subst b
-      and c' = subst_glob_constr subst c in
+      let po' = Option.Smart.map (subst_glob_constr env subst) po
+      and b' = subst_glob_constr env subst b
+      and c' = subst_glob_constr env subst c in
 	if po' == po && b' == b && c' == c then raw else
           GLetTuple (nal,(na,po'),b',c')
 
   | GIf (c,(na,po),b1,b2) as raw ->
-      let po' = Option.Smart.map (subst_glob_constr subst) po
-      and b1' = subst_glob_constr subst b1
-      and b2' = subst_glob_constr subst b2
-      and c' = subst_glob_constr subst c in
+      let po' = Option.Smart.map (subst_glob_constr env subst) po
+      and b1' = subst_glob_constr env subst b1
+      and b2' = subst_glob_constr env subst b2
+      and c' = subst_glob_constr env subst c in
 	if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else
           GIf (c',(na,po'),b1',b2')
 
   | GRec (fix,ida,bl,ra1,ra2) as raw ->
-      let ra1' = Array.Smart.map (subst_glob_constr subst) ra1
-      and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in
+      let ra1' = Array.Smart.map (subst_glob_constr env subst) ra1
+      and ra2' = Array.Smart.map (subst_glob_constr env subst) ra2 in
       let bl' = Array.Smart.map
         (List.Smart.map (fun (na,k,obd,ty as dcl) ->
-          let ty' = subst_glob_constr subst ty in
-          let obd' = Option.Smart.map (subst_glob_constr subst) obd in
+          let ty' = subst_glob_constr env subst ty in
+          let obd' = Option.Smart.map (subst_glob_constr env subst) obd in
           if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
@@ -1116,8 +1115,8 @@ let rec subst_glob_constr subst = DAst.map (function
     else GHole (nknd, naming, nsolve)
 
   | GCast (r1,k) as raw ->
-      let r1' = subst_glob_constr subst r1 in
-      let k' = smartmap_cast_type (subst_glob_constr subst) k in
+      let r1' = subst_glob_constr env subst r1 in
+      let k' = smartmap_cast_type (subst_glob_constr env subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
 
   )
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 8695d52b12..425fd5096e 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -37,7 +37,7 @@ val print_allow_match_default_clause : bool ref
 
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
-val subst_glob_constr : substitution -> glob_constr -> glob_constr
+val subst_glob_constr : env -> substitution -> glob_constr -> glob_constr
 
 val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g
 
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'))
 
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 36317b3acf..90a536e780 100644
--- a/pretyping/patternops.mli
+++ b/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 : substitution -> constr_pattern -> constr_pattern
+val subst_pattern : Environ.env -> substitution -> constr_pattern -> constr_pattern
 
 val noccurn_pattern : int -> constr_pattern -> bool