Merge tag 'upstream/8.5_beta1+dfsg'

Upstream version 8.5~beta1+dfsg

1 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v
index fd5d139c..445ffac8 100644
--- a/test-suite/success/Case11.v
+++ b/test-suite/success/Case11.v
@@ -1,5 +1,5 @@
-(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
-(* Problème rapporté par Solange Coupet *)
+(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
+(* Problème rapporté par Solange Coupet *)
 
 Section A.
 
@@ -7,7 +7,7 @@ Variables (Alpha : Set) (Beta : Set).
 
 Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) :
   Alpha * Beta := match c with
-                  | existS a b => (a, b)
+                  | existS _ a b => (a, b)
                   end.
 
 End A.