diff options
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 13e1abacc1..f72eb2acbe 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -378,6 +378,10 @@ let fold_map f accu c = match kind c with let accu, l' = Array.smartfoldmap f accu l in if b'==b && l'==l then accu, c else accu, mkApp (b', l') + | Proj (p,t) -> + let accu, t' = f accu t in + if t' == t then accu, c + else accu, mkProj (p, t') | Evar (e,l) -> let accu, l' = Array.smartfoldmap f accu l in if l'==l then accu, c |