UIP in SProp

1 files changed, 10 insertions, 9 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index b39ec37cd1..b713d7812e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -75,7 +75,8 @@ type cbv_value =
 and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
-  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+  | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert
+            * case_info * cbv_value subs * cbv_stack
   | PROJ of Projection.t * cbv_stack
 
 (* les vars pourraient etre des constr,
@@ -134,7 +135,7 @@ let rec stack_concat stk1 stk2 =
   match stk1 with
       TOP -> stk2
     | APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
-    | CASE(c,b,i,s,stk1') -> CASE(c,b,i,s,stack_concat stk1' stk2)
+    | CASE(c,b,iv,i,s,stk1') -> CASE(c,b,iv,i,s,stack_concat stk1' stk2)
     | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2)
 
 (* merge stacks when there is no shifts in between *)
@@ -339,9 +340,9 @@ let rec reify_stack t = function
   | TOP -> t
   | APP (args,st) ->
       reify_stack (mkApp(t,Array.map reify_value args)) st
-  | CASE (ty,br,ci,env,st) ->
+  | CASE (ty,br,iv,ci,env,st) ->
       reify_stack
-        (mkCase (ci, ty, t,br))
+        (mkCase (ci, ty, iv, t, br))
         st
   | PROJ (p, st) ->
        reify_stack (mkProj (p, t)) st
@@ -400,7 +401,7 @@ let rec norm_head info env t stack =
                         they could be computed when getting out of the stack *)
       let nargs = Array.map (cbv_stack_term info TOP env) args in
       norm_head info env head (stack_app nargs stack)
-  | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
+  | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack))
   | Cast (ct,_,_) -> norm_head info env ct stack
 
   | Proj (p, c) ->
@@ -514,14 +515,14 @@ and cbv_stack_value info env = function
         cbv_stack_term info stk envf redfix
 
     (* constructor in a Case -> IOTA *)
-    | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
+    | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk)))
             when red_set info.reds fMATCH ->
         let cargs =
           Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
-    | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
+    | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk))
             when red_set info.reds fMATCH ->
                     cbv_stack_term info stk env br.(n-1)
 
@@ -597,9 +598,9 @@ let rec apply_stack info t = function
   | TOP -> t
   | APP (args,st) ->
       apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
-  | CASE (ty,br,ci,env,st) ->
+  | CASE (ty,br,iv,ci,env,st) ->
       apply_stack info
-        (mkCase (ci, cbv_norm_term info env ty, t,
+        (mkCase (ci, cbv_norm_term info env ty, iv, t,
                     Array.map (cbv_norm_term info env) br))
         st
   | PROJ (p, st) ->