From 0f1e73d09a2d1f5116b49a90f94297f98a70f9a3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 4 May 2014 11:46:12 +0200
Subject: Add missing case for primitive projection in fold_map.

---
 kernel/constr.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3