From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 kernel/mod_subst.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/mod_subst.ml')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 317141e324..2aeb1ea202 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -364,20 +364,21 @@ let rec map_kn f f' c =
       | Construct (((kn,i),j),u) ->
           let kn' = f kn in
           if kn'==kn then c else mkConstructU (((kn',i),j),u)
-      | Case (ci,p,ct,l) ->
+      | Case (ci,p,iv,ct,l) ->
           let ci_ind =
             let (kn,i) = ci.ci_ind in
             let kn' = f kn in
             if kn'==kn then ci.ci_ind else kn',i
           in
           let p' = func p in
+          let iv' = map_invert func iv in
           let ct' = func ct in
           let l' = Array.Smart.map func l in
-            if (ci.ci_ind==ci_ind && p'==p
+            if (ci.ci_ind==ci_ind && p'==p && iv'==iv
                 && l'==l && ct'==ct)then c
             else
               mkCase ({ci with ci_ind = ci_ind},
-                      p',ct', l')
+                      p',iv',ct', l')
       | Cast (ct,k,t) ->
           let ct' = func ct in
           let t'= func t in
-- 
cgit v1.2.3