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.

---
 kernel/nativecode.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index bd659a471f..041751ecfe 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1923,7 +1923,8 @@ let rec compile_deps env sigma prefix ~interactive init t =
       comp_stack, (mind_updates, const_updates)
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
-      compile_deps env sigma prefix ~interactive init (mkApp (mkConst p, [|c|]))
+    let term = mkApp (mkConst (Projection.constant p), [|c|]) in
+      compile_deps env sigma prefix ~interactive init term
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
-- 
cgit v1.2.3