From 754775e39b5fa0342a1f4a46cbce0fc98d569d9d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 22 Jul 2015 17:26:49 +0200
Subject: Extraction: fix primitive projection extraction.

Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
---
 test-suite/success/primitiveproj.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 068f8ac3cc..125615c535 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -188,3 +188,10 @@ Set Printing All.
 Check (@p' nat).
 Check p'.
 Unset Printing All.
+
+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.
+Recursive Extraction term term'.
+(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file
-- 
cgit v1.2.3