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.

1 files changed, 7 insertions, 5 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index cfe46152e..b65fdb3ac 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -342,13 +342,15 @@ let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind_of_term c with
       | Const kn -> (try snd (f' kn) with No_subst -> c)
-      | Proj (kn,t) -> 
-          let kn' = try fst (f' (kn,Univ.Instance.empty))
-	    with No_subst -> kn 
+      | Proj (p,t) -> 
+          let p' = 
+	    try
+	      Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p
+	    with No_subst -> p
 	  in
 	  let t' = func t in
-	    if kn' == kn && t' == t then c
-	    else mkProj (kn', t')
+	    if p' == p && t' == t then c
+	    else mkProj (p', t')
       | Ind ((kn,i),u) ->
 	  let kn' = f kn in
 	  if kn'==kn then c else mkIndU ((kn',i),u)