From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 test-suite/success/primitiveproj.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'test-suite/success/primitiveproj.v')

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 2fa77049..31a1608c 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -1,5 +1,5 @@
 Set Primitive Projections.
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 Module Prim.
 
 Record F := { a : nat; b : a = a }.
@@ -181,7 +181,10 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
 
 Definition term (x : wrap nat) := x.(unwrap).
 Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
+
+Require Coq.extraction.Extraction.
 Recursive Extraction term term'.
+Extraction TestCompile term term'.
 (*Unset Printing Primitive Projection Parameters.*)
 
 (* Primitive projections in the presence of let-ins (was not failing in beta3)*)
-- 
cgit v1.2.3