Merge PR #10390: UIP in SProp

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

1 files changed, 2 insertions, 2 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index c4472050f8..1cf5be10ae 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None
+    | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ -> None
   in
   hdrec c
 
@@ -163,7 +163,7 @@ let hdchar env sigma c =
         let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
         lowercase_first_char id
     | Evar _ (* We could do better... *)
-    | Meta _ | Case (_, _, _, _) -> "y"
+    | Meta _ | Case _ -> "y"
     | Int _ -> "i"
     | Float _ -> "f"
   in