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/bugs/closed/4710.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'test-suite/bugs/closed/4710.v')

diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
index fdc85010..e792a362 100644
--- a/test-suite/bugs/closed/4710.v
+++ b/test-suite/bugs/closed/4710.v
@@ -1,8 +1,9 @@
+Require Coq.extraction.Extraction.
+
 Set Primitive Projections.
 Record Foo' := Foo { foo : nat }.
 Extraction foo.
 Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
-Extraction Language Ocaml.
 Extraction foo2p.
 
 Definition bla (x : Foo2 0) := foo2p _ x.
@@ -10,3 +11,5 @@ Extraction bla.
 
 Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
 Extraction bla'.
+
+Extraction TestCompile foo foo2p bla bla'.
-- 
cgit v1.2.3