universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes

 This file, which is currently expected to fail at the last line
 (with Universe Inconsistency), was actually failing earlier
 after Pierre Boutillier changed the patterns (parameters are required now).

 A final "Fail" will soon arrives here to avoid such issue in the future...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v
index a8b5b975b..c101339a6 100644
--- a/test-suite/failure/universes-buraliforti-redef.v
+++ b/test-suite/failure/universes-buraliforti-redef.v
@@ -230,14 +230,14 @@ End Burali_Forti_Paradox.
 intros.
 change
   match i0 X1 R1, i0 X2 R2 with
-  | i1 x1 r1, i1 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
+  | i1 _ _ x1 r1, i1 _ _ x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
   end.
 case H; simpl.
 exists (fun x : X1 => x).
 red; trivial.
 Defined.
 
-(* The following command raises 'Error: Universe Inconsistency'.
+(* The following command should raise 'Error: Universe Inconsistency'.
    To allow large elimination of A0, i0 must not be a large constructor.
    Hence, the constraint Type_j' < Type_i' is added, which is incompatible
    with the constraint j >= i in the paradox.