From 84544396cbbf34848be2240acf181b4d5f1f42d2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 27 Sep 2014 16:08:02 +0200
Subject: Add a boolean to indicate the unfolding state of a primitive
 projection, so as to reproduce correctly the reduction behavior of existing
 projections, i.e. delta + iota. Make [projection] an abstract datatype in
 Names.ml, most of the patch is about using that abstraction. Fix
 unification.ml which tried canonical projections too early in presence of
 primitive projections.

---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index bbbc9bce70..aa0232d19e 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -617,7 +617,7 @@ 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 p Univ.Instance.empty (c :: args)
+        extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: 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