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.

20 files changed, 144 insertions, 102 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 726e64e811..c9c6cecb1d 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 4c1e3c3af2..d491ded727 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 f754f9f3fe..73534210cd 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 e39b2bba42..1db7bbd619 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 6a48d84edc..0ae8736433 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 7af6396336..b0f1dd920a 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 07540af57b..0b0ff2fb59 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 e27ee84aa0..ddaf69676a 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 9f460d08f9..6e32d70c09 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 245c7f9437..a6c0149a4e 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 829fa106c5..60db95e25f 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 01317ba253..9b77266927 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 cfe71510a1..382357a8d1 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 5c18297c0b..8c4dbfd984 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 4c9fc4dc53..fb66923a65 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 6672c7fa7e..9a9b347516 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 3374da327e..b16cf75f5d 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 0088563fab..a2584571db 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 c1347c9b49..d6926dac30 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 3f7f238c41..0501035423 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