diff options
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index cfe46152ef..b65fdb3aca 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -342,13 +342,15 @@ let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with | Const kn -> (try snd (f' kn) with No_subst -> c) - | Proj (kn,t) -> - let kn' = try fst (f' (kn,Univ.Instance.empty)) - with No_subst -> kn + | Proj (p,t) -> + let p' = + try + Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p + with No_subst -> p in let t' = func t in - if kn' == kn && t' == t then c - else mkProj (kn', t') + if p' == p && t' == t then c + else mkProj (p', t') | Ind ((kn,i),u) -> let kn' = f kn in if kn'==kn then c else mkIndU ((kn',i),u) |