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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fa7dd105c7..5421020d2a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -184,7 +184,8 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) args =
 let judge_of_constant env cst =
   judge_of_constant_knowing_parameters env cst [||]
 
-let type_of_projection env (cst,u) =
+let type_of_projection env (p,u) =
+  let cst = Projection.constant p in
   let cb = lookup_constant cst env in
   match cb.const_proj with
   | Some pb -> 
-- 
cgit v1.2.3