diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-05-04 11:46:12 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:02 +0200 |
commit | 0f1e73d09a2d1f5116b49a90f94297f98a70f9a3 (patch) | |
tree | 1a735f23e2aefcbbb2da1c33059367d04b3bd942 /kernel/constr.ml | |
parent | 8dfcf43a839b2e893818b67702a3ee305971a624 (diff) |
Add missing case for primitive projection in fold_map.
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 13e1abacc..f72eb2acb 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 |