Merge PR #10390: UIP in SProp

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 366203faeb..0206d4e70d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -208,7 +208,7 @@ let occur_rigidly flags env evd (evk,_) t =
       if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true
       else Reducible
     | Rel _ | Var _ -> Reducible
-    | Case (_,_,c,_) ->
+    | Case (_,_,_,c,_) ->
       (match aux c with
       | Rigid b -> Rigid b
       | _ -> Reducible)
@@ -382,7 +382,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       else None, x in
     match sk1, sk2 with
     | [], [] -> None, Success i
-    | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
+    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
       (match f env i CONV t1 t2 with
       | Success i' ->
         (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
@@ -417,7 +417,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
   let rec ise_stack2 i sk1 sk2 =
     match sk1, sk2 with
     | [], [] -> Success i
-    | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 ->
+    | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 ->
       ise_and i [
       (fun i -> ise_stack2 i q1 q2);
       (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);