aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/tacsubst.ml4
-rw-r--r--plugins/ssr/ssrview.ml2
-rw-r--r--pretyping/detyping.ml49
-rw-r--r--pretyping/detyping.mli2
-rw-r--r--pretyping/patternops.ml44
-rw-r--r--pretyping/patternops.mli2
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/redexpr.ml2
8 files changed, 53 insertions, 54 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index caaa547a07..8fb238aecb 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x
let subst_declared_or_quantified_hypothesis _ x = x
let subst_glob_constr_and_expr subst (c, e) =
- (Detyping.subst_glob_constr subst c, e)
+ (Detyping.subst_glob_constr (Global.env()) subst c, e)
let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
@@ -99,7 +99,7 @@ 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 subst p)
+ (bvars,subst_glob_constr subst c,subst_pattern (Global.env()) subst p)
let subst_redexp subst =
Redops.map_red_expr_gen
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 537fd7d7b4..075ebf006a 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -43,7 +43,7 @@ module AdaptorDb = struct
term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
let subst_adaptor ( subst, (k, t as a)) =
- let t' = Detyping.subst_glob_constr subst t in
+ let t' = Detyping.subst_glob_constr (Global.env()) subst t in
if t' == t then a else k, t'
let in_db =
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
diff --git a/tactics/hints.ml b/tactics/hints.ml
index f49b1660b8..7eeee7ee07 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1064,7 +1064,7 @@ 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 subst) data.pat in
+ let pat' = Option.Smart.map (subst_pattern (Global.env()) 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) ->
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index aabfae444e..7ff88bb4b7 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -262,7 +262,7 @@ let subst_red_expr subs =
Redops.map_red_expr_gen
(subst_mps subs)
(Mod_subst.subst_evaluable_reference subs)
- (Patternops.subst_pattern subs)
+ (Patternops.subst_pattern (Global.env()) subs)
let inReduction : bool * string * red_expr -> obj =
declare_object
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:02:45 +0000