From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- test-suite/success/Case11.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test-suite/success/Case11.v') diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v index 445ffac8..fbe909ec 100644 --- a/test-suite/success/Case11.v +++ b/test-suite/success/Case11.v @@ -5,9 +5,9 @@ Section A. Variables (Alpha : Set) (Beta : Set). -Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) : +Definition nodep_prod_of_dep (c : sigT (fun a : Alpha => Beta)) : Alpha * Beta := match c with - | existS _ a b => (a, b) + | existT _ a b => (a, b) end. End A. -- cgit v1.2.3