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.

55 files changed, 317 insertions, 218 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6bf294967..2cbac2175 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -239,7 +239,7 @@ let constr_display csr =
   | Construct (((sp,i),j),u) ->
       "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
-  | Proj (p, c) -> "Proj("^(string_of_con p)^","^term_display c ^")"
+  | Proj (p, c) -> "Proj("^(string_of_con (Projection.constant p))^","^term_display c ^")"
   | Case (ci,p,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display bl)^")"
@@ -328,7 +328,7 @@ let print_pure_constr csr =
       print_string ","; universes_display u;
       print_string ")"
   | Proj (p,c') -> print_string "Proj(";
-      sp_con_display p;
+      sp_con_display (Projection.constant p);
       print_string ",";
       box_display c';
       print_string ")"
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 885b0e6b4..63461c11a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -983,7 +983,8 @@ let rec glob_of_pat env sigma = function
       GVar (loc,id)
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None)
   | PMeta (Some n) -> GPatVar (loc,(false,n))
-  | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env sigma c])
+  | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
+			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
       GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 56780e240..6b3de2621 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -684,14 +684,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	(* [id] a goal variable *)
 	GVar (loc,id), [], [], []
 
-let is_projection_ref = function
-  | ConstRef r -> 
-    if Environ.is_projection r (Global.env ()) then 
-      let pb = Environ.lookup_projection r (Global.env ()) in
-	Some (r, pb.Declarations.proj_npars)
-    else None
-  | _ -> None
-
 let proj_impls r impls =
   let env = Global.env () in
   let f (x, l) = x, projection_implicits env r l in
@@ -710,17 +702,15 @@ let find_appl_head_data c =
   | GRef (loc,ref,_) as x -> 
     let impls = implicits_of_global ref in
     let scopes = find_arguments_scope ref in
-    let isproj = is_projection_ref ref in
-      x, isproj, impls, scopes, []
+      x, impls, scopes, []
   | GApp (_,GRef (_,ref,_),l) as x
       when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
       let impls = implicits_of_global ref in 
       let scopes = find_arguments_scope ref in
-      let isproj = is_projection_ref ref in
-	x, isproj, List.map (drop_first_implicits n) impls,
+	x, List.map (drop_first_implicits n) impls,
 	List.skipn_at_least n scopes,[]
-  | x -> x,None,[],[],[]
+  | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
   user_err_loc (loc,"",str "Abbreviation is not applied enough.")
@@ -777,26 +767,24 @@ let intern_applied_reference intern env namedctx lvar us args = function
 	try intern_qualid loc qid intern env lvar us args
 	with Not_found -> error_global_not_found_loc loc qid
       in
-      let x, isproj, imp, scopes, l = find_appl_head_data r in
-      let isproj = if projapp then isproj else None in
-	(x,imp,scopes,l), isproj, args2
+      let x, imp, scopes, l = find_appl_head_data r in
+	(x,imp,scopes,l), args2
   | Ident (loc, id) ->
-      try intern_var env lvar namedctx loc id, None, args
+      try intern_var env lvar namedctx loc id, args
       with Not_found ->
       let qid = qualid_of_ident id in
       try
 	let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in
-	let x, isproj, imp, scopes, l = find_appl_head_data r in
-	let isproj = if projapp then isproj else None in
-	  (x,imp,scopes,l), isproj, args2
+	let x, imp, scopes, l = find_appl_head_data r in
+	  (x,imp,scopes,l), args2
       with Not_found ->
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || env.unb then
-	  (GVar (loc,id), [], [], []), None, args
+	  (GVar (loc,id), [], [], []), args
 	else error_global_not_found_loc loc qid
 
 let interp_reference vars r =
-  let (r,_,_,_),_,_ =
+  let (r,_,_,_),_ =
     intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
       {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env} []
@@ -1358,11 +1346,11 @@ let extract_explicit_arg imps args =
 let internalize globalenv env allow_patvar lvar c =
   let rec intern env = function
     | CRef (ref,us) as x ->
-	let (c,imp,subscopes,l),isproj,_ =
+	let (c,imp,subscopes,l),_ =
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
 	    lvar us [] ref 
 	in
-	  apply_impargs (None, isproj) c env imp subscopes l (constr_loc x)
+	  apply_impargs c env imp subscopes l (constr_loc x)
 
     | CFix (loc, (locid,iddef), dl) ->
         let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
@@ -1457,7 +1445,7 @@ let internalize globalenv env allow_patvar lvar c =
 	intern {env with tmp_scope = None;
 		  scopes = find_delimiters_scope loc key :: env.scopes} e
     | CAppExpl (loc, (isproj,ref,us), args) ->
-        let (f,_,args_scopes,_),isprojf,args =
+        let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
 	    lvar us args ref 
@@ -1466,23 +1454,23 @@ let internalize globalenv env allow_patvar lvar c =
 	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
 
     | CApp (loc, (isproj,f), args) ->
-        let isproj,f,args = match f with
+        let f,args = match f with
           (* Compact notations like "t.(f args') args" *)
-          | CApp (_,(Some _ as isproj',f), args') when not (Option.has_some isproj) -> 
-	    isproj',f,args'@args
+          | CApp (_,(Some _,f), args') when not (Option.has_some isproj) -> 
+	    f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
-          | _ -> isproj,f,args in
-	let (c,impargs,args_scopes,l),isprojf,args =
+          | _ -> f,args in
+	let (c,impargs,args_scopes,l),args =
           match f with
             | CRef (ref,us) -> 
 	       intern_applied_reference intern env
 		 (Environ.named_context globalenv) lvar us args ref
             | CNotation (loc,ntn,([],[],[])) ->
                 let c = intern_notation intern env lvar loc ntn ([],[],[]) in
-                let x, isproj, impl, scopes, l = find_appl_head_data c in
-		  (x,impl,scopes,l), None, args
-            | x -> (intern env f,[],[],[]), None, args in
-          apply_impargs (isproj,isprojf) c env impargs args_scopes 
+                let x, impl, scopes, l = find_appl_head_data c in
+		  (x,impl,scopes,l), args
+            | x -> (intern env f,[],[],[]), args in
+          apply_impargs c env impargs args_scopes 
 	    (merge_impargs l args) loc
 
     | CRecord (loc, _, fs) ->
@@ -1719,7 +1707,7 @@ let internalize globalenv env allow_patvar lvar c =
 	  intern_args env subscopes rargs
     in aux 1 l subscopes eargs rargs
 
-  and apply_impargs (isproj,isprojf) c env imp subscopes l loc = 
+  and apply_impargs c env imp subscopes l loc = 
     let imp = select_impargs_size (List.length l) imp in
     let l = intern_impargs c env imp subscopes l in
       smart_gapp c loc l
diff --git a/interp/notation.ml b/interp/notation.ml
index 6cc99ddb4..e765701d4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -535,7 +535,7 @@ let compute_scope_class t =
   let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in
   match kind_of_term t' with
   | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t')
-  | Proj (p, c) -> ScopeRef (ConstRef p)
+  | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p))
   | Sort _ -> ScopeSort
   |  _ -> raise Not_found
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 36a022fd9..6fd1c689f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -501,11 +501,12 @@ let rec compile_constr reloc c sz cont =
   | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
   | Proj (p,c) -> 
     (* compile_const reloc p [|c|] sz cont *)
-    let cb = lookup_constant p !global_env in
+    let kn = Projection.constant p in
+    let cb = lookup_constant kn !global_env in
       (* TODO: better representation of projections *)
     let pb = Option.get cb.const_proj in
     let args = Array.make pb.proj_npars mkProp in
-      compile_const reloc p Univ.Instance.empty (Array.append args [|c|]) sz cont
+      compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
 
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 14afcc4db..23861347a 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -88,6 +88,7 @@ module type RedFlagsSig = sig
   val red_add_transparent : reds -> transparent_state -> reds
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
+  val red_projection : reds -> projection -> bool
 end
 
 module RedFlags = (struct
@@ -168,6 +169,10 @@ module RedFlags = (struct
     | DELTA -> (* Used for Rel/Var defined in context *)
 	incr_cnt red.r_delta delta
 
+  let red_projection red p = 
+    if Projection.unfolded p then true
+    else red_set red (fCONST (Projection.constant p))
+
 end : RedFlagsSig)
 
 open RedFlags
@@ -338,7 +343,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
@@ -708,7 +713,7 @@ let rec zip m stk rem = match stk with
   let t = FCases(ci, p, m, br) in
   zip {norm=neutr m.norm; term=t} s rem
 | Zproj (i,j,cst) :: s -> 
-  zip {norm=neutr m.norm; term=FProj (cst,m)} s rem
+  zip {norm=neutr m.norm; term=FProj (Projection.make cst true,m)} s rem
 | Zfix(fx,par)::s ->
   zip fx par ((Zapp [|m|] :: s) :: rem)
 | Zshift(n)::s ->
@@ -876,7 +881,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
       (** Try to drop the params, might fail on partially applied constructors. *)
       let argss = try_drop_parameters depth pars args in
       let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					 term = FProj (p, right) }) projs in
+					 term = FProj (Projection.make p true, right) }) projs in
 	argss, [Zapp hstack]	
     | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
@@ -932,11 +937,13 @@ let rec knh info m stk =
            | (None, stk') -> (m,stk'))
     | FCast(t,_,_) -> knh info t stk
     | FProj (p,c) ->
-        if red_set info.i_flags (fCONST p) then
+      let unf = Projection.unfolded p in
+        if unf || red_set info.i_flags (fCONST (Projection.constant p)) then
           (match try Some (lookup_projection p (info_env info)) with Not_found -> None with
 	  | None -> (m, stk)
 	  | Some pb ->
-	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
+	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+				Projection.constant p)
 			 :: zupdate m stk))
 	else (m,stk)
 
@@ -1033,7 +1040,7 @@ let rec zip_term zfun m stk =
         let t = mkCase(ci, zfun p, m, Array.map zfun br) in
         zip_term zfun t s
     | Zproj(_,_,p)::s -> 
-        let t = mkProj (p, m) in 
+        let t = mkProj (Projection.make p true, m) in 
 	zip_term zfun t s
     | Zfix(fx,par)::s ->
         let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 1062d0e61..445fcb7bc 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -64,7 +64,10 @@ module type RedFlagsSig = sig
 
   (** Tests if a reduction kind is set *)
   val red_set : reds -> red_kind -> bool
-
+    
+  (** This tests if the projection is in unfolded state already or
+      is unfodable due to delta. *)
+  val red_projection : reds -> projection -> bool
 end
 
 module RedFlags : RedFlagsSig
@@ -113,7 +116,7 @@ type fterm =
   | FInd of inductive puniverses
   | FConstruct of constructor puniverses
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 2a13f938b..912067629 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -85,7 +85,7 @@ type ('constr, 'types) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
 type t = (t,t) kind_of_term
@@ -486,7 +486,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 =
     Int.equal (Array.length l1) (Array.length l2) &&
       f c1 c2 && Array.equal f l1 l2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && f c1 c2
+  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && f c1 c2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
   | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
   | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
@@ -523,7 +523,7 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
   | App (c1,l1), App (c2,l2) ->
     Int.equal (Array.length l1) (Array.length l2) &&
       eq c1 c2 && Array.equal eq l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && eq c1 c2
+  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
   | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
@@ -657,7 +657,7 @@ let constr_ord_int f t1 t2 =
     | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
     | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
     | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
-    | Proj (p1,c1), Proj (p2,c2) -> (con_ord =? f) p1 p2 c1 c2
+    | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
     | Evar (e1,l1), Evar (e2,l2) ->
         (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
     | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2
@@ -820,8 +820,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 	(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Proj (p,c) ->
         let c, hc = sh_rec c in
-	let p' = sh_con p in
-	  (Proj (p', c), combinesmall 17 (combine (Constant.hash p') hc))
+	let p' = Projection.hashcons p in
+	  (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc))
       | Const (c,u) ->
 	let c' = sh_con c in
 	let u', hu = sh_instance u in
@@ -906,7 +906,7 @@ let rec hash t =
     | App (c,l) ->
       combinesmall 7 (combine (hash_term_array l) (hash c))
     | Proj (p,c) ->
-      combinesmall 17 (combine (Constant.hash p) (hash c))
+      combinesmall 17 (combine (Projection.hash p) (hash c))
     | Evar (e,l) ->
       combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
     | Const (c,u) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 58f248b03..da7ac6a0d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -103,7 +103,7 @@ val mkConst : constant -> constr
 val mkConstU : pconstant -> constr
 
 (** Constructs a projection application *)
-val mkProj : (constant * constr) -> constr
+val mkProj : (projection * constr) -> constr
 
 (** Inductive types *)
 
@@ -190,7 +190,7 @@ type ('constr, 'types) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 
 (** User view of [constr]. For [App], it is ensured there is at
    least one argument and the function is not itself an applicative
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2d316fc1d..5f6aebc4e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -123,12 +123,13 @@ let expmod_constr cache modlist c =
 
       | Proj (p, c') ->
           (try 
-	     let p' = share_univs (ConstRef p) Univ.Instance.empty modlist in
+	     let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
+	     let make c = Projection.make c (Projection.unfolded p) in
 	     match kind_of_term p' with
-	     | Const (p',_) -> mkProj (p', substrec c')
+	     | Const (p',_) -> mkProj (make p', substrec c')
 	     | App (f, args) -> 
 	       (match kind_of_term f with 
-	       | Const (p', _) -> mkProj (p', substrec c')
+	       | Const (p', _) -> mkProj (make p', substrec c')
 	       | _ -> assert false)
 	     | _ -> assert false
 	   with Not_found -> map_constr substrec c)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6b0b0bdba..b331d8da7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -328,7 +328,7 @@ let template_polymorphic_pconstant (cst,u) env =
   else template_polymorphic_constant cst env
 
 let lookup_projection cst env =
-  match (lookup_constant cst env).const_proj with 
+  match (lookup_constant (Projection.constant cst) env).const_proj with 
   | Some pb -> pb
   | None -> anomaly (Pp.str "lookup_projection: constant is not a projection")
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4feec40e8..73a23ef05 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -692,14 +692,15 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
 	let ty = substl subst (liftn 1 j t) in
-	let term = mkProj (kn, mkRel 1) in
+	let term = mkProj (Projection.make kn true, mkRel 1) in
+	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
 	let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
 	let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
 		     proj_arg = i; proj_type = ty; proj_eta = etab, etat; 
 		     proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs, term :: subst)
+	  (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
       | Anonymous -> raise UndefinableExpansion
   in
   let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
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)
diff --git a/kernel/names.ml b/kernel/names.ml
index c76d95937..5d73bd520 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -782,7 +782,33 @@ let kn_ord = KerName.compare
 (** Compatibility layer for [Constant] *)
 
 type constant = Constant.t
-type projection = constant
+
+
+module Projection = 
+struct 
+  type t = constant * bool
+    
+  let make c b = (c, b)
+
+  let constant = fst
+  let unfolded = snd
+  let unfold (c, b as p) = if b then p else (c, true)
+  let equal (c, b) (c', b') = Constant.equal c c' && b == b'
+  let hash (c, b) = (if b then 0 else 1) + Constant.hash c
+  let hashcons (c, b as x) = 
+    let c' = hcons_con c in 
+      if c' == c then x else (c', b)
+
+  let compare (c, b) (c', b') =
+    if b == b' then Constant.CanOrd.compare c c'
+    else if b then 1 else -1
+
+  let map f (c, b as x) =
+    let c' = f c in
+      if c' == c then x else (c', b)
+end
+
+type projection = Projection.t
 
 let constant_of_kn = Constant.make1
 let constant_of_kn_equiv = Constant.make
diff --git a/kernel/names.mli b/kernel/names.mli
index 49a838ae5..893cad09d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -634,7 +634,25 @@ val kn_ord : kernel_name -> kernel_name -> int
 type constant = Constant.t
 (** @deprecated Alias type *)
 
-type projection = constant
+module Projection : sig
+  type t
+    
+  val make : constant -> bool -> t
+
+  val constant : t -> constant
+  val unfolded : t -> bool
+  val unfold : t -> t
+
+  val equal : t -> t -> bool
+  val hash : t -> int
+  val hashcons : t -> t
+
+  val compare : t -> t -> int
+    
+  val map : (constant -> constant) -> t -> t
+end
+
+type projection = Projection.t
 
 val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
 (** @deprecated Same as [Constant.make] *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index bd659a471..041751ecf 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
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 34ed33f94..ba45c329f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -586,7 +586,8 @@ let rec lambda_of_constr env sigma c =
   | Construct _ ->  lambda_of_app env sigma c empty_args
 
   | Proj (p, c) ->
-      mkLapp (Lproj (get_const_prefix !global_env p, p)) [|lambda_of_constr env sigma c|]
+    let kn = Projection.constant p in
+      mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|]
 
   | Case(ci,t,a,branches) ->  
       let (mind,i as ind) = ci.ci_ind in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 802d2b67b..9a7146890 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -275,12 +275,14 @@ let in_whnf (t,stk) =
     | FLOCKED -> assert false
 
 let unfold_projection infos p c =
-  if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then
-    (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with
-    | Some pb -> 
-      let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
-	Some (c, s)
-    | None -> None)
+  let unf = Projection.unfolded p in
+    if unf || RedFlags.red_set infos.i_flags (RedFlags.fCONST (Projection.constant p)) then
+      (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with
+      | Some pb -> 
+	let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+		       Projection.constant p) in
+	  Some (c, s)
+      | None -> None)
   else None
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
@@ -368,7 +370,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	| Some (def2,s2) ->
 	  eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
 	| None -> 
-          if eq_constant p1 p2 && compare_stack_shape v1 v2 then
+          if Projection.equal p1 p2 && compare_stack_shape v1 v2 then
 	    let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
 	      convert_stacks l2r infos lft1 lft2 v1 v2 u1
 	  else (* Two projections in WHNF: unfold *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 3b6b69a28..ab678666f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -89,7 +89,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 
 type values = Constr.values
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 5ff5f9ba1..28ebc41e2 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -86,7 +86,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of constant * 'constr
+  | Proj      of projection * 'constr
 
 type values = Constr.values
 
@@ -405,7 +405,7 @@ val mkLambda : Name.t * types * constr -> constr
 val mkLetIn : Name.t * constr * types * constr -> constr
 val mkApp : constr * constr array -> constr
 val mkConst : constant -> constr
-val mkProj : (constant * constr) -> constr
+val mkProj : projection * constr -> constr
 val mkInd : inductive -> constr
 val mkConstruct : constructor -> constr
 val mkConstU : constant puniverses -> constr
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fa7dd105c..5421020d2 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 -> 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 976380ede..3f9345ff8 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -203,7 +203,9 @@ let rec conv_eq env pb t1 t2 cu =
 	else raise NotConvertible
     | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu
     | Proj (p1,c1), Proj (p2,c2) ->
-	if eq_constant p1 p2 then conv_eq env pb c1 c2 cu else raise NotConvertible
+	if eq_constant (Projection.constant p1) (Projection.constant p2) then
+	  conv_eq env pb c1 c2 cu 
+	else raise NotConvertible
     | Ind c1, Ind c2 ->
        eq_puniverses eq_ind c1 c2 cu
     | Construct c1, Construct c2 ->
diff --git a/library/heads.ml b/library/heads.ml
index 31908816b..8b28f0500 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -84,7 +84,7 @@ let kind_of_head env t =
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
   | App (c,al) -> aux k (Array.to_list al @ l) c b
   | Proj (p,c) ->
-      (try on_subterm k (c :: l) b (constant_head p)
+      (try on_subterm k (c :: l) b (constant_head (Projection.constant p))
        with Not_found -> assert false)
 
   | Case (_,_,c,_) -> aux k [] c true
diff --git a/library/universes.ml b/library/universes.ml
index 7fe4258c2..cc0153311 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -220,7 +220,7 @@ let compare_head_gen_proj env equ eqs eqc' m n =
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
     (match kind_of_term f with
-    | Const (p', u) when eq_constant p p' -> 
+    | Const (p', u) when eq_constant (Projection.constant p) p' -> 
       let pb = Environ.lookup_projection p env in
       let npars = pb.Declarations.proj_npars in
 	if Array.length args == npars + 1 then
@@ -429,7 +429,7 @@ let global_app_of_constr c =
   | Ind (i, u) -> (IndRef i, u), None
   | Construct (c, u) -> (ConstructRef c, u), None
   | Var id -> (VarRef id, Instance.empty), None
-  | Proj (p, c) -> (ConstRef p, Instance.empty), Some c
+  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
   | _ -> raise Not_found
 
 open Declarations
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 50b647e44..5a4a435a5 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -425,15 +425,15 @@ and applist_proj c l =
 and applist_projection c l =
   match kind_of_term c with
   | Const c when Environ.is_projection (fst c) (Global.env()) ->
+    let p = Projection.make (fst c) false in
     (match l with 
     | [] -> (* Expand the projection *)
-      let kn = fst c in
       let ty,_ = Typeops.type_of_constant (Global.env ()) c in
-      let pb = Environ.lookup_projection kn (Global.env()) in
+      let pb = Environ.lookup_projection p (Global.env()) in
       let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
-	it_mkLambda_or_LetIn (mkProj(kn,mkRel 1)) ctx
+	it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
     | hd :: tl ->
-      applistc (mkProj (fst c, hd)) tl)
+      applistc (mkProj (p, hd)) tl)
   | _ -> applistc c l
 
 let rec canonize_name c =
@@ -456,9 +456,10 @@ let rec canonize_name c =
 	  mkLetIn (na, func b,func t,func ct)
       | App (ct,l) ->
 	  mkApp (func ct,Array.smartmap func l)
-      | Proj(kn,c) ->
-        let canon_const = constant_of_kn (canonical_con kn) in 
-	  (mkProj (canon_const, func c))
+      | Proj(p,c) ->
+	let p' = Projection.map (fun kn ->
+          constant_of_kn (canonical_con kn)) p in 
+	  (mkProj (p', func c))
       | _ -> c
 
 (* rebuild a term from a pattern and a substitution *)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 45d6a9393..364a71d28 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -78,8 +78,9 @@ let rec decompose_term env sigma t=
 	let canon_const = constant_of_kn (canonical_con c) in 
 	  (Symb (mkConstU (canon_const,u)))
     | Proj (p, c) -> 
-	let canon_const = constant_of_kn (canonical_con p) in 
-	  (Appli (Symb (mkConst canon_const), decompose_term env sigma c))
+	let canon_const kn = constant_of_kn (canonical_con kn) in 
+	let p' = Projection.map canon_const p in
+	  (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->if closed0 t then (Symb t) else raise Not_found
 
 (* decompose equality in members and type *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index bbbc9bce7..aa0232d19 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]. *)
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 745e190cb..ed7f18001 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args)
+          PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> snd (pattern_of_constr Evd.empty c)
+      | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
   in
   aux bodyi
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 726e64e81..c9c6cecb1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1283,7 +1283,8 @@ let mk_case pb (ci,pred,c,brs) =
   let mib = lookup_mind (fst ci.ci_ind) pb.env in
     match mib.mind_record with
     | Some (cs, pbs) when Array.length pbs > 0 -> 
-      Reduction.beta_appvect brs.(0) (Array.map (fun p -> mkProj (p, c)) cs)
+      Reduction.beta_appvect brs.(0) 
+	(Array.map (fun p -> mkProj (Projection.make p false, c)) cs)
     | _ -> mkCase (ci,pred,c,brs)
 
 (**********************************************************************)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 4c1e3c3af..d491ded72 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -197,7 +197,7 @@ let rec norm_head info env t stack =
   | Cast (ct,_,_) -> norm_head info env ct stack
   
   | Proj (p, c) -> 
-    let pinfo = Option.get ((Environ.lookup_constant p (info_env info)).Declarations.const_proj) in
+    let pinfo = Environ.lookup_projection p (info_env info) in
     norm_head info env c (PROJ (p, pinfo, stack))
 
   (* constants, axioms
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f754f9f3f..73534210c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -31,7 +31,7 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of constant
   | CL_IND of inductive
-  | CL_PROJ of projection
+  | CL_PROJ of constant
 
 type cl_info_typ = {
   cl_param : int
@@ -196,7 +196,8 @@ let find_class_type sigma t =
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, Univ.Instance.empty, args
     | Const (sp,u) -> CL_CONST sp, u, args
-    | Proj (p, c) -> CL_PROJ p, Univ.Instance.empty, c :: args
+    | Proj (p, c) when not (Projection.unfolded p) ->
+      CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args
     | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
     | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, []
     | Sort _ -> CL_SORT, Univ.Instance.empty, []
@@ -406,7 +407,7 @@ let reference_arity_length ref =
 
 let projection_arity_length p =
   let len = reference_arity_length (ConstRef p) in
-  let pb = Environ.lookup_projection p (Global.env ()) in 
+  let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in 
     len - pb.Declarations.proj_npars
 
 let class_params = function
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index e39b2bba4..1db7bbd61 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -19,7 +19,7 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of constant
   | CL_IND of inductive
-  | CL_PROJ of projection
+  | CL_PROJ of constant
 
 (** Equality over [cl_typ] *)
 val cl_typ_eq : cl_typ -> cl_typ -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6a48d84ed..0ae873643 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -350,7 +350,7 @@ let apply_coercion env sigma p hj typ_cl =
 	    (if isid then
 	      { uj_val = ja.uj_val; uj_type = jres.uj_type }
 	     else if isproj then
-	       { uj_val = mkProj (fst (destConst fv.uj_val), ja.uj_val); 
+	       { uj_val = mkProj (Projection.make (fst (destConst fv.uj_val)) false, ja.uj_val); 
 		 uj_type = jres.uj_type }
 	     else
 	      jres),
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index 7af639633..b0f1dd920 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -227,10 +227,10 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	   
       | PApp (c1,arg1), App (c2,arg2) ->
 	(match c1, kind_of_term c2 with
-	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) ->
+	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) ->
 	  raise PatternMatchingFailure
 	| PProj (pr1,c1), Proj (pr,c) ->
-	  if eq_constant pr1 pr then 
+	  if eq_constant (Projection.constant pr1) (Projection.constant pr) then 
 	    try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2
 	    with Invalid_argument _ -> raise PatternMatchingFailure
 	  else raise PatternMatchingFailure
@@ -241,14 +241,16 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
           try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure)
 	  
-      | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 pr) -> 
+      | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 
+								(Projection.constant pr)) -> 
 	raise PatternMatchingFailure
 	
       | PApp (c, args), Proj (pr, c2) ->
 	let term = Retyping.expand_projection env sigma pr c2 [] in
 	  sorec stk env subst p term
 
-      | PProj (p1,c1), Proj (p2,c2) when eq_constant p1 p2 ->
+      | PProj (p1,c1), Proj (p2,c2) when 
+	  eq_constant (Projection.constant p1) (Projection.constant p2) ->
           sorec stk env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 07540af57..0b0ff2fb5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -445,12 +445,22 @@ let rec detype flags avoid env sigma t =
     | Proj (p,c) ->
       if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
 	(* lax mode, used by debug printers only *) 
-	GApp (dl, GRef (dl, ConstRef p, None), 
+	GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), 
 	      [detype flags avoid env sigma c])
-      else let ty = Retyping.get_type_of (snd env) sigma c in
-	   let (ind, args) = Inductive.find_rectype (snd env) ty in
-	     GApp (dl, GRef (dl, ConstRef p, None), 
-		   List.map (detype flags avoid env sigma) (args @ [c]))
+      else 
+	if Projection.unfolded p then
+	  (** Print the compatibility match version *)
+	  let pb = Environ.lookup_projection p (snd env) in
+	  let body = pb.Declarations.proj_body in
+	  let ty = Retyping.get_type_of (snd env) sigma c in
+	  let (ind, args) = Inductive.find_rectype (snd env) ty in
+	  let body' = strip_lam_assum body in
+	    detype flags avoid env sigma (substl (c :: List.rev args) body')
+	else
+	  let ty = Retyping.get_type_of (snd env) sigma c in
+	  let (ind, args) = Inductive.find_rectype (snd env) ty in
+	    GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), 
+		  List.map (detype flags avoid env sigma) (args @ [c]))
     | Evar (evk,cl) ->
       let id,l =
         try Evd.evar_ident evk sigma,
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e27ee84aa..ddaf69676 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -33,18 +33,24 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> debug_unification:=a);
 }
 
-let unfold_projection env p c stk =
+let unfold_projection env ts p c stk =
   (match try Some (lookup_projection p env) with Not_found -> None with
   | Some pb -> 
+    let cst = Projection.constant p in
     let unfold () = 
-      let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
+      let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+			  Projection.constant p) in
 	Some (c, s :: stk)
     in
-      (match ReductionBehaviour.get (Globnames.ConstRef p) with
-      | None -> unfold ()
-      | Some (recargs, nargs, flags) ->
-	if (List.mem `ReductionNeverUnfold flags) then None
-	else unfold ())
+      if Projection.unfolded p then unfold ()
+      else 
+	if is_transparent_constant ts cst then
+	  (match ReductionBehaviour.get (Globnames.ConstRef cst) with
+	  | None -> unfold ()
+	  | Some (recargs, nargs, flags) ->
+	    if (List.mem `ReductionNeverUnfold flags) then None
+	    else unfold ())
+	else None
   | None -> None)
 
 let eval_flexible_term ts env c stk =
@@ -64,10 +70,7 @@ let eval_flexible_term ts env c stk =
        with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c, stk)
   | Lambda _ -> Some (c, stk)
-  | Proj (p, c) -> 
-    if is_transparent_constant ts p
-    then unfold_projection env p c stk
-    else None
+  | Proj (p, c) -> unfold_projection env ts p c stk
   | _ -> assert false
 
 type flex_kind_of_term =
@@ -527,7 +530,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	in
 	ise_try evd [f1; f2]
 
-	| Proj (p, c), Proj (p', c') when eq_constant p p' ->
+	| Proj (p, c), Proj (p', c') when Projection.equal p p' ->
 	  let f1 i = 
 	    ise_and i 
 	    [(fun i -> evar_conv_x ts env i CONV c c');
@@ -539,7 +542,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  in
 	    ise_try evd [f1; f2]
 	      
-	| Proj (p, t), Const (p',_) when eq_constant p p' ->
+	| Proj (p, t), Const (p',_) when eq_constant (Projection.constant p) p' ->
 	  let f1 i = 
 	    let pb = Environ.lookup_projection p env in
 	      (match Stack.strip_n_app pb.Declarations.proj_npars sk2' with
@@ -554,7 +557,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    in evar_eqappr_x ts env i pbty out1 out2
 	  in ise_try evd [f1;f2]
 
-	| Const (p',_), Proj (p, t) when eq_constant p p' ->
+	| Const (p',_), Proj (p, t) when eq_constant  (Projection.constant p) p' ->
 	  let f1 i = 
 	    let pb = Environ.lookup_projection p env in
 	      (match Stack.strip_n_app pb.Declarations.proj_npars sk1' with
@@ -801,7 +804,7 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
 	   let l1' = Stack.tail pars sk1 in
 	   let l2' = 
 	     let term = Stack.zip (term2,sk2) in 
-	       List.map (fun p -> mkProj (p, term)) (Array.to_list projs)
+	       List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs)
 	   in
 	     exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' 
 	       (Stack.append_app_list l2' Stack.empty)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 9f460d08f..6e32d70c0 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -104,7 +104,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 	| None -> mkCase (ci, lift ndepar p,  mkRel 1,
 			  Termops.rel_vect ndepar k)
 	| Some ps -> 
-	  let term = mkApp (mkRel 2, Array.map (fun p -> mkProj (p, mkRel 1)) ps) in
+	  let term = mkApp (mkRel 2, 
+			    Array.map (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
 	    if dep then
 	      let ty = mkApp (mkRel 3, [| mkRel 1 |]) in 
 		mkCast (term, DEFAULTcast, ty)
@@ -390,7 +391,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 		    let n, subst = 
 		      List.fold_right (fun (na,b,t) (i, subst) ->
 			if b == None then 
-			  let t = mkProj (ps.(i), mkRel 1) in
+			  let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
 			    (i + 1, t :: subst)
 			else (i, mkRel 0 :: subst))
 			ctx (0, [])
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 245c7f943..a6c0149a4 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -83,7 +83,7 @@ let head_name c = (* Find the head constant of a constr if any *)
     match kind_of_term c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
     | Cast (c,_,_) | App (c,_) -> hdrec c
-    | Proj (kn,_) -> Some (Label.to_id (con_label kn))
+    | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
     | Const _ | Ind _ | Construct _ | Var _ ->
 	Some (basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
@@ -104,7 +104,7 @@ let hdchar env c =
     match kind_of_term c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
     | Cast (c,_,_) | App (c,_) -> hdrec k c
-    | Proj (kn,_)
+    | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
     | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
     | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
     | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 829fa106c..60db95e25 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -268,7 +268,7 @@ and nf_atom env atom =
   | Aevar (ev,_) -> mkEvar ev
   | Aproj(p,c) ->
       let c = nf_accu env c in
-      mkProj(p,c)
+	mkProj(Projection.make p false,c)
   | _ -> fst (nf_atom_type env atom)
 
 and nf_atom_type env atom =
@@ -342,7 +342,7 @@ and nf_atom_type env atom =
   | Aproj(p,c) ->
       let c,tc = nf_accu_type env c in
       let cj = make_judge c tc in
-      let uj = Typeops.judge_of_projection env p cj in
+      let uj = Typeops.judge_of_projection env (Projection.make p true) cj in
       uj.uj_val, uj.uj_type
 
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 01317ba25..9b7726692 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -106,7 +106,7 @@ let rec head_pattern_bound t =
     | PCase (_,p,c,br) -> head_pattern_bound c
     | PRef r         -> r
     | PVar id        -> VarRef id
-    | PProj (p,c)    -> ConstRef p
+    | PProj (p,c)    -> ConstRef (Projection.constant p)
     | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
@@ -120,7 +120,7 @@ let head_of_constr_reference c = match kind_of_term c with
   | Var id -> VarRef id
   | _ -> anomaly (Pp.str "Not a rigid reference")
 
-let pattern_of_constr sigma t =
+let pattern_of_constr env sigma t =
   let ctx = ref [] in
   let rec pattern_of_constr t =
   match kind_of_term t with
@@ -150,7 +150,8 @@ let pattern_of_constr sigma t =
     | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
-    | Proj (p, c) -> PProj (constant_of_kn(canonical_con p), pattern_of_constr c)
+    | Proj (p, c) -> PProj (Projection.map (fun kn -> constant_of_kn(canonical_con kn)) p,
+			    pattern_of_constr c)
     | Evar (evk,ctxt as ev) ->
         (match snd (Evd.evar_source evk sigma) with
           | Evar_kinds.MatchingVar (b,id) ->
@@ -203,7 +204,7 @@ let error_instantiate_pattern id l =
     ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
-let instantiate_pattern sigma lvar c =
+let instantiate_pattern env sigma lvar c =
   let rec aux vars = function
   | PVar id as x ->
       (try
@@ -215,7 +216,7 @@ let instantiate_pattern sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  snd (pattern_of_constr sigma c)
+	  snd (pattern_of_constr env sigma c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -240,13 +241,13 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 snd (pattern_of_constr Evd.empty t)
+	 snd (pattern_of_constr (Global.env()) Evd.empty t)
   | PVar _
   | PEvar _
   | PRel _ -> pat
   | PProj (p,c) -> 
-      let p',t = subst_global subst (ConstRef p) in
-      let p' = destConstRef p' in
+      let p' = Projection.map (fun p -> 
+	destConstRef (fst (subst_global subst (ConstRef p)))) p in
       let c' = subst_pattern subst c in
 	if p' == p && c' == c then pat else
 	  PProj(p',c')
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cfe71510a..382357a8d 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,7 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
@@ -48,7 +48,7 @@ val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
 val pattern_of_glob_constr : glob_constr ->
       patvar list * constr_pattern
 
-val instantiate_pattern :
+val instantiate_pattern : Environ.env ->
   Evd.evar_map -> extended_patvar_map ->
   constr_pattern -> constr_pattern
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5c18297c0..8c4dbfd98 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -566,6 +566,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     let app_f = 
       match kind_of_term fj.uj_val with
       | Const (p, u) when Environ.is_projection p env ->
+	let p = Projection.make p false in
 	let pb = Environ.lookup_projection p env in
 	let npars = pb.Declarations.proj_npars in
 	  fun n -> 
@@ -705,7 +706,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	let rec aux n k names l =
 	  match names, l with
 	  | na :: names, ((_, None, t) :: l) -> 
-	    (na, Some (lift (cs.cs_nargs - n) (mkProj (ps.(cs.cs_nargs - k), cj.uj_val))), t)
+	    let proj = Projection.make ps.(cs.cs_nargs - k) false in
+	      (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t)
 	    :: aux (n+1) (k + 1) names l
 	  | na :: names, ((_, c, t) :: l) -> 
 	    (na, c, t) :: aux (n+1) k names l
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4c9fc4dc5..fb66923a6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -208,7 +208,7 @@ sig
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * projection
+  | Proj of int * int * constant
   | Fix of fixpoint * 'a t * Cst_stack.t
   | Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t
   | Shift of int
@@ -262,7 +262,7 @@ struct
   type 'a member =
   | App of 'a app_node
   | Case of Term.case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * projection
+  | Proj of int * int * constant
   | Fix of fixpoint * 'a t * Cst_stack.t
   | Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t
   | Shift of int
@@ -302,7 +302,7 @@ struct
 	if Univ.Instance.is_empty u then Constant.print c
 	else str"(" ++ Constant.print c ++ str ", " ++ Univ.Instance.pr u ++ str")"
       | Cst_proj (p, c) ->
-	pr_c c ++ str".(" ++ Constant.print p ++ str")"
+	pr_c c ++ str".(" ++ Constant.print (Projection.constant p) ++ str")"
 
   let empty = []
   let is_empty = CList.is_empty
@@ -329,7 +329,7 @@ struct
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
 	Constant.equal c1 c2 && Univ.Instance.equal u1 u2
       | Cst_proj (p1,c1), Cst_proj (p2,c2) ->
-	Constant.equal p1 p2 && f (c1,lft1) (c2,lft2)
+	Projection.equal p1 p2 && f (c1,lft1) (c2,lft2)
       | _, _ -> false
     in
     let rec equal_rec sk1 lft1 sk2 lft2  =
@@ -347,7 +347,7 @@ struct
 	then equal_rec s1 lft1 s2 lft2
 	else None
       | (Proj (n1,m1,p)::s1, Proj(n2,m2,p2)::s2) ->
-	if Int.equal n1 n2 && Int.equal m1 m2 && Names.Constant.CanOrd.equal p p2
+	if Int.equal n1 n2 && Int.equal m1 m2 && Constant.equal p p2
 	then equal_rec s1 lft1 s2 lft2
 	else None
       | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
@@ -537,7 +537,7 @@ struct
   | f, (Cst (cst,_,_,params,_)::s) ->
     zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s)))
   | f, (Shift n::s) -> zip ~refold (lift n f, s)
-  | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (p,f),s)
+  | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (Projection.make p true,f),s)
   | _, (Update _::_) -> assert false
 end
 
@@ -829,13 +829,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		    | Some (bef,arg,s') ->
 		      whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s')
        )
-    | Proj (p, c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) ->
+    | Proj (p, c) when Closure.RedFlags.red_projection flags p ->
       (let pb = lookup_projection p env in
+       let kn = Projection.constant p in
        let npars = pb.Declarations.proj_npars 
        and arg = pb.Declarations.proj_arg in
-	 match ReductionBehaviour.get (Globnames.ConstRef p) with
+	 match ReductionBehaviour.get (Globnames.ConstRef kn) with
 	 | None ->
-	   let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in
+	   let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in
 	     whrec Cst_stack.empty(* cst_l *) stack'
 	 | Some (recargs, nargs, flags) ->
 	   if (List.mem `ReductionNeverUnfold flags
@@ -850,7 +851,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	       |[] -> (* if nargs has been specified *)
 		(* CAUTION : the constant is NEVER refold
                    (even when it hides a (co)fix) *)
-		 let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in
+		 let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in
 		   whrec Cst_stack.empty(* cst_l *) stack'
 	       | curr::remains -> 
 		 if curr == 0 then (* Try to reduce the record argument *)
@@ -931,7 +932,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		match Stack.strip_n_app 0 stack with
 		| None -> assert false
 		| Some (_,arg,s'') ->
-		  whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p) :: s''))
+		  whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,Projection.constant p) :: s''))
 	  | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with
 	    | None -> fold ()
 	    | Some (bef,arg,s''') ->
@@ -984,9 +985,10 @@ let local_whd_state_gen flags sigma =
 	| _ -> s)
       | _ -> s)
 
-    | Proj (p,c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) ->
+    | Proj (p,c) when Closure.RedFlags.red_projection flags p ->
       (let pb = lookup_projection p (Global.env ()) in
-	 whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
+	 whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+			       Projection.constant p)
            :: stack))
 
     | Case (ci,p,d,lf) ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 6672c7fa7..9a9b34751 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -57,7 +57,7 @@ module Stack : sig
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * projection
+  | Proj of int * int * constant
   | Fix of fixpoint * 'a t * Cst_stack.t
   | Cst of 'a cst_member * int (** current foccussed arg *) * int list (** remaining args *)
     * 'a t * Cst_stack.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3374da327..b16cf75f5 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -245,5 +245,5 @@ let sorts_of_context env evc ctxt =
 let expand_projection env sigma pr c args =
   let ty = get_type_of env sigma c in
   let (i,u), ind_args = Inductive.find_rectype env ty in
-    mkApp (mkConstU (pr,u), 
+    mkApp (mkConstU (Projection.constant pr,u), 
 	   Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 0088563fa..a2584571d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -585,7 +585,7 @@ let reduce_proj env sigma whfun whfun' c =
 	(match kind_of_term constr with
 	| Construct _ -> 
 	  let proj_narg = 
-	    let pb = Option.get ((lookup_constant proj env).Declarations.const_proj) in
+	    let pb = lookup_projection proj env in
 	      pb.Declarations.proj_npars + pb.Declarations.proj_arg
 	  in List.nth cargs proj_narg
 	| _ -> raise Redelimination)
@@ -738,24 +738,26 @@ and whd_simpl_stack env sigma =
 
       | Proj (p, c) ->
         (try 
-	   if is_evaluable env (EvalConstRef p) then
-	     let pb = Option.get ((lookup_constant p env).Declarations.const_proj) in
- 	       (match ReductionBehaviour.get (ConstRef p) with
- 	       | Some (l, n, f) when List.mem `ReductionNeverUnfold f -> (* simpl never *) s'
-	       | Some (l, n, f) when not (List.is_empty l) ->
-		 let l' = List.map_filter (fun i -> 
-		   let idx = (i - (pb.Declarations.proj_npars + 1)) in
-		     if idx < 0 then None else Some idx) l in
-		 let stack = reduce_params env sigma stack l' in
-		   (match reduce_projection env sigma pb 
-		     (whd_construct_stack env sigma c) stack 
-		    with
-		    | Reduced s' -> redrec (applist s')
-		    | NotReducible -> s')
- 	       | _ ->
-		 match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with
-		 | Reduced s' -> redrec (applist s')
-		 | NotReducible -> s')
+	   let unf = Projection.unfolded p in
+	     if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
+	       let pb = lookup_projection p env in
+ 		 (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with
+ 		 | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> 
+                   (* simpl never *) s'
+		 | false, Some (l, n, f) when not (List.is_empty l) ->
+		   let l' = List.map_filter (fun i -> 
+		     let idx = (i - (pb.Declarations.proj_npars + 1)) in
+		       if idx < 0 then None else Some idx) l in
+		   let stack = reduce_params env sigma stack l' in
+		     (match reduce_projection env sigma pb 
+		       (whd_construct_stack env sigma c) stack 
+		      with
+		      | Reduced s' -> redrec (applist s')
+		      | NotReducible -> s')
+ 		 | _ ->
+		   match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with
+		   | Reduced s' -> redrec (applist s')
+		   | NotReducible -> s')
 	   else s'
 	 with Redelimination -> s')
 	  
@@ -826,12 +828,10 @@ let try_red_product env sigma c =
 	  | Construct _ -> c
 	  | _ -> redrec env c
 	in
-	  (match match_eval_proj env p with
-	  | Some pb -> 
-            (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with
-	    | Reduced s -> simpfun (applist s)
-	    | NotReducible -> raise Redelimination)
-	  | None -> raise Redelimination)
+	let pb = lookup_projection p env in
+          (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with
+	  | Reduced s -> simpfun (applist s)
+	  | NotReducible -> raise Redelimination)
       | _ -> 
         (match match_eval_ref env x with
         | Some (ref, u) ->
@@ -920,7 +920,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
       | CoFix _ | Fix _ -> s'
       | Proj (p,c) when
 	  (match kind_of_term constr with
-	  | Const (c', _) -> eq_constant p c'
+	  | Const (c', _) -> eq_constant (Projection.constant p) c'
 	  | _ -> false) ->
 	let pb = Environ.lookup_projection p env in
 	  if List.length stack <= pb.Declarations.proj_npars then
@@ -947,7 +947,7 @@ let simpl env sigma c = strong whd_simpl env sigma c
 let matches_head env sigma c t =
   match kind_of_term t with
     | App (f,_) -> ConstrMatching.matches env sigma c f
-    | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst p)
+    | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst (Projection.constant p))
     | _ -> raise ConstrMatching.PatternMatchingFailure
 
 let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index c1347c9b4..d6926dac3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -79,7 +79,7 @@ let rec pr_constr c = match kind_of_term c with
   | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")"
   | Construct (((sp,i),j),u) ->
       str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
-  | Proj (p,c) -> str"Proj(" ++ pr_con p ++ str"," ++ pr_constr c ++ str")"
+  | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
   | Case (ci,p,c,bl) -> v 0
       (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
              pr_constr c ++ str"of") ++ cut() ++
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3f7f238c4..050103542 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -370,7 +370,7 @@ let use_metas_pattern_unification flags nb l =
 
 type key = 
   | IsKey of Closure.table_key
-  | IsProj of constant * constr
+  | IsProj of projection * constr
 
 let expand_table_key env = function
   | ConstKey cst -> constant_opt_value_in env cst
@@ -380,7 +380,8 @@ let expand_table_key env = function
 let unfold_projection env p stk =
   (match try Some (lookup_projection p env) with Not_found -> None with
   | Some pb -> 
-    let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
+    let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+			Projection.constant p) in
       s :: stk
   | None -> assert false)
 
@@ -405,7 +406,8 @@ let key_of env b flags f =
   | Var id when is_transparent env (VarKey id) && 
       Id.Pred.mem id (fst flags.modulo_delta) ->
     Some (IsKey (VarKey id))
-  | Proj (p, c) when Cpred.mem p (snd flags.modulo_delta) ->
+  | Proj (p, c) when Projection.unfolded p
+      || Cpred.mem (Projection.constant p) (snd flags.modulo_delta) ->
     Some (IsProj (p, c))
   | _ -> None
   
@@ -417,7 +419,7 @@ let translate_key = function
 
 let translate_key = function
   | IsKey k -> translate_key k    
-  | IsProj (c, _) -> ConstKey c
+  | IsProj (c, _) -> ConstKey (Projection.constant c)
   
 let oracle_order env cf1 cf2 =
   match cf1 with
@@ -430,8 +432,10 @@ let oracle_order env cf1 cf2 =
       | None -> Some true
       | Some k2 ->
 	match k1, k2 with
-	| IsProj (p, _), IsKey (ConstKey (p',_)) when eq_constant p p' -> Some false
-	| IsKey (ConstKey (p,_)), IsProj (p', _) when eq_constant p p' -> Some true
+	| IsProj (p, _), IsKey (ConstKey (p',_)) 
+	  when eq_constant (Projection.constant p) p' -> Some false
+	| IsKey (ConstKey (p,_)), IsProj (p', _) 
+	  when eq_constant p (Projection.constant p') -> Some true
 	| _ ->
           Some (Conv_oracle.oracle_order (Environ.oracle env) false
 		  (translate_key k1) (translate_key k2))
@@ -508,7 +512,7 @@ let eta_constructor_app env f l1 term =
       | Some (projs, _) ->
         let pars = mib.Declarations.mind_nparams in
 	let l1' = Array.sub l1 pars (Array.length l1 - pars) in
-	let l2 = Array.map (fun p -> mkProj (p, term)) projs in
+	let l2 = Array.map (fun p -> mkProj (Projection.make p false, term)) projs in
 	  l1', l2
       | _ -> assert false)
   | _ -> assert false
@@ -666,11 +670,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
              | Some l ->
 	         solve_pattern_eqn_array curenvnb f2 l cM substn)
 
-	| App (f1,l1), App (f2,l2) ->
-            unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
-
 	| Proj (p1,c1), Proj (p2,c2) ->
-	    if eq_constant p1 p2 then
+	    if eq_constant (Projection.constant p1) (Projection.constant p2) then
 	      try 
 		let substn = unirec_rec curenvnb CONV true wt substn c1 c2 in
 		  try (* Force unification of the types to fill in parameters *)
@@ -679,6 +680,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 		      unify_0_with_initial_metas substn true env cv_pb 
 			{ flags with modulo_conv_on_closed_terms = Some full_transparent_state;
 			  modulo_delta = full_transparent_state;
+			  modulo_eta = true;
 			  modulo_betaiota = true }
 			ty1 ty2
 		  with RetypeError _ -> substn
@@ -687,6 +689,23 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	    else
 	      unify_not_same_head curenvnb pb b wt substn cM cN
 
+	| App (f1, l1), Proj (p', c) when isConst f1 && 
+	    eq_constant (fst (destConst f1)) (Projection.constant p') -> 
+	  expand curenvnb pb b false substn cM f1 l1 cN cN [||]
+
+	| Proj (p', c), App (f1, l1) when isConst f1 && 
+	    eq_constant (fst (destConst f1)) (Projection.constant p') -> 
+	  expand curenvnb pb b false substn cM f1 l1 cN cN [||]
+
+	| App (f1,l1), App (f2,l2) ->
+	  (match kind_of_term f1, kind_of_term f2 with
+	  | Const (p, u), Proj (p', c) when eq_constant p (Projection.constant p') -> 
+	    expand curenvnb pb b false substn cM f1 l1 cN f2 l2
+	  | Proj (p', _), Const (p, _) when eq_constant p (Projection.constant p') ->
+	    expand curenvnb pb b false substn cM f1 l1 cN f2 l2
+	  | _ ->
+            unify_app curenvnb pb b substn cM f1 l1 cN f2 l2)
+
 	| _ ->
             unify_not_same_head curenvnb pb b wt substn cM cN
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6fa4342d3..564e111e0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -198,7 +198,7 @@ let strip_params env c =
 	(match cb.Declarations.const_proj with
 	| Some pb -> 
 	  let n = pb.Declarations.proj_npars in
-	    mkApp (mkProj (p, args.(n)), 
+	    mkApp (mkProj (Projection.make p false, args.(n)), 
 		   Array.sub args (n+1) (Array.length args - (n + 1)))
 	| None -> c)
     | _ -> c)
@@ -585,7 +585,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = snd (Patternops.pattern_of_constr sigma cty) in
+	let pat = snd (Patternops.pattern_of_constr env sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -604,7 +604,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible dummy_goal.sigma ctx in
         let ce = mk_clenv_from { dummy_goal with sigma = sigma' } (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = snd (Patternops.pattern_of_constr sigma c') in
+	let pat = snd (Patternops.pattern_of_constr env sigma c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -701,7 +701,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (snd (Patternops.pattern_of_constr sigma (clenv_type ce)));
+              pat = Some (snd (Patternops.pattern_of_constr env sigma (clenv_type ce)));
 	      name = name;
               code=Res_pf_THEN_trivial_fail(c,t,ctx) })
   
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 5fbc6f5b2..ef813744e 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -33,7 +33,7 @@ type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
 let decomp_pat =
   let rec decrec acc = function
     | PApp (f,args) -> decrec (Array.to_list args @ acc) f
-    | PProj (p, c) -> (PRef (ConstRef p), c :: acc)
+    | PProj (p, c) -> (PRef (ConstRef (Projection.constant p)), c :: acc)
     | c -> (c,acc)
   in
   decrec []
@@ -41,7 +41,7 @@ let decomp_pat =
 let decomp =
   let rec decrec acc c = match kind_of_term c with
     | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-    | Proj (p, c) -> (mkConst p, c :: acc)
+    | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc)
     | Cast (c1,_,_) -> decrec acc c1
     | _ -> (c,acc)
   in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e25a862dd..991eac57e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -584,7 +584,7 @@ let interp_pure_open_constr ist =
 let interp_typed_pattern ist env sigma (c,_) =
   let sigma, c =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
-  pattern_of_constr sigma c
+  pattern_of_constr env sigma c
 
 (* Interprets a constr expression casted by the current goal *)
 let pf_interp_casted_constr ist gl c =
@@ -986,7 +986,7 @@ let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
     snd (interp_typed_pattern ist env sigma c)
   else
-    instantiate_pattern sigma lfun pat
+    instantiate_pattern env sigma lfun pat
 
 let read_pattern lfun ist env sigma = function
   | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 23b649809..69a72db4f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -124,7 +124,7 @@ let head_constr_bound t =
   let hd,args = decompose_app ccl in
   match kind_of_term hd with
     | Const _ | Ind _ | Construct _ | Var _ -> hd
-    | Proj (p, _) -> mkConst p
+    | Proj (p, _) -> mkConst (Projection.constant p)
     | _ -> raise Bound
 
 let head_constr c =
@@ -139,7 +139,7 @@ let decompose_app_bound t =
     | Ind (i,u) -> IndRef i, args
     | Construct (c,u) -> ConstructRef c, args
     | Var id -> VarRef id, args
-    | Proj (p, c) -> ConstRef p, Array.cons c args
+    | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args
     | _ -> raise Bound
 
 (******************************************)
@@ -1172,7 +1172,7 @@ let make_projection env sigma params cstr sign elim i n c u =
 	  let args = extended_rel_vect 0 sign in
 	  let proj =
 	    if Environ.is_projection proj env then
-	      mkProj (proj, mkApp (c, args))
+	      mkProj (Projection.make proj false, mkApp (c, args))
 	    else
 	      mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
 		[|mkApp (c, args)|])
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index f8d7a197b..9826ecdff 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -288,7 +288,7 @@ struct
       Array.fold_left (fun c a -> Term (DApp (c,a)))
         (pat_of_constr f) (Array.map pat_of_constr ca)
     | Proj (p,c) -> 
-        Term (DApp (Term (DRef (ConstRef p)), pat_of_constr c))
+        Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
 
     and ctx_of_constr ctx c = match kind_of_term c with
     | Prod (_,t,c)   -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v
index f962e1f04..ed8964ce1 100644
--- a/test-suite/bugs/opened/3660.v
+++ b/test-suite/bugs/opened/3660.v
@@ -18,10 +18,10 @@ admit.
 Defined.
 Local Open Scope equiv_scope.
 Axiom equiv_path : forall (A B : Type) (p : A = B), A <~> B.
+
 Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))).
   intros.
   change (IsEquiv (equiv_path C D o @ap _ _ setT C D)).
   apply @isequiv_compose; [ | admit ].
-  solve [ apply isequiv_ap_setT ].
-  Undo.
-  Fail typeclasses eauto.
+  Set Typeclasses Debug. 
+  typeclasses eauto.
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 177aa1cd6..7694869a5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -266,7 +266,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 		  (** Already defined in the kernel silently *)
 		let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
 		  Declare.definition_message fid;
-		  kn, mkProj (kn,mkRel 1)
+		  kn, mkProj (Projection.make kn false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
 		let body = match optci with