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.
---
 plugins/extraction/extraction.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 080512b273..6ae519ef60 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -633,7 +633,8 @@ let rec extract_term env mle mlt c args =
     | Construct (cp,u) ->
 	extract_cons_app env mle mlt cp u args
     | Proj (p, c) ->
-        extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
+        let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
+	  extract_term env mle mlt term args
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
-- 
cgit v1.2.3