In evarconv and unification, expand folded primitive projections to

their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.

11 files changed, 145 insertions, 112 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ddaf69676..a8ab0666d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -33,27 +33,33 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> debug_unification:=a);
 }
 
-let unfold_projection env ts p c stk =
+let unfold_projection env evd 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, 
-			  Projection.constant p) in
+			  p, Cst_stack.empty) in
 	Some (c, s :: stk)
     in
+    let unfold_app () =
+      let t' = Retyping.expand_projection env evd p c [] in
+      let f, args = destApp t' in
+      let stk = Stack.append_app args stk in
+	Some (f, stk)
+    in
       if Projection.unfolded p then unfold ()
       else 
 	if is_transparent_constant ts cst then
 	  (match ReductionBehaviour.get (Globnames.ConstRef cst) with
-	  | None -> unfold ()
+	  | None -> unfold_app ()
 	  | Some (recargs, nargs, flags) ->
 	    if (List.mem `ReductionNeverUnfold flags) then None
-	    else unfold ())
+	    else unfold_app ())
 	else None
   | None -> None)
 
-let eval_flexible_term ts env c stk =
+let eval_flexible_term ts env evd c stk =
   match kind_of_term c with
   | Const (c,u as cu) ->
       if is_transparent_constant ts c
@@ -70,7 +76,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) -> unfold_projection env ts p c stk
+  | Proj (p, c) -> unfold_projection env evd ts p c stk
   | _ -> assert false
 
 type flex_kind_of_term =
@@ -78,10 +84,10 @@ type flex_kind_of_term =
   | MaybeFlexible of Constr.t * Constr.t Stack.t (* reducible but not necessarily reduced *)
   | Flexible of existential
 
-let flex_kind_of_term ts env c sk =
+let flex_kind_of_term ts env evd c sk =
   match kind_of_term c with
     | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
-      Option.cata (fun (x,y) -> MaybeFlexible (x,y)) Rigid (eval_flexible_term ts env c sk)
+      Option.cata (fun (x,y) -> MaybeFlexible (x,y)) Rigid (eval_flexible_term ts env evd c sk)
     | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible (c, sk)
     | Evar ev -> Flexible ev
     | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid
@@ -143,7 +149,8 @@ let check_conv_record (t1,sk1) (t2,sk2) =
       match kind_of_term t2 with
 	Prod (_,a,b) -> (* assert (l2=[]); *)
       	  if dependent (mkRel 1) b then raise Not_found
-	  else lookup_canonical_conversion (proji, Prod_cs),(Stack.append_app [|a;pop b|] Stack.empty)
+	  else lookup_canonical_conversion (proji, Prod_cs),
+	    (Stack.append_app [|a;pop b|] Stack.empty)
       | Sort s ->
 	lookup_canonical_conversion
 	  (proji, Sort_cs (family_of_sort s)),[]
@@ -254,8 +261,9 @@ let ise_stack2 no_app env evd f sk1 sk2 =
 	| Success i'' -> ise_stack2 true i'' q1 q2
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
-    | Stack.Proj (n1,a1,p1)::q1, Stack.Proj (n2,a2,p2)::q2 ->
-       if eq_constant p1 p2 then ise_stack2 true i q1 q2
+    | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
+       if eq_constant (Projection.constant p1) (Projection.constant p2)
+       then ise_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
       Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
@@ -297,8 +305,9 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 	  (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
 	  (fun i -> ise_stack2 i a1 a2)]
       else UnifFailure (i,NotSameHead)
-    | Stack.Proj (n1,a1,p1)::q1, Stack.Proj (n2,a2,p2)::q2 ->
-       if eq_constant p1 p2 then ise_stack2 i q1 q2
+    | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
+       if eq_constant (Projection.constant p1) (Projection.constant p2)
+       then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
     | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
@@ -394,7 +403,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let out1 = whd_betaiota_deltazeta_for_iota_state
       (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
-      (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), Cst_stack.empty in
+      (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), 
+      Cst_stack.empty in
     if onleft then evar_eqappr_x ts env' evd CONV out1 out2
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
@@ -461,7 +471,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     let open Pp in
 	     pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) 
 		 ++ fnl ()) in
-  match (flex_kind_of_term (fst ts) env term1 sk1, flex_kind_of_term (fst ts) env term2 sk2) with
+  match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
 	  match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
@@ -541,36 +551,6 @@ 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]
-	      
-	| 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
-	      | Some (pars, t', rest) ->
-		ise_and i
-		  [(fun i -> evar_conv_x ts env i CONV t t');
-		   (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 rest)]
-	      | None -> UnifFailure (evd, NotSameHead))
-	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
-            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
-	    in evar_eqappr_x ts env i pbty out1 out2
-	  in ise_try evd [f1;f2]
-
-	| 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
-	      | Some (pars, t', rest) ->
-		ise_and i
-		  [(fun i -> evar_conv_x ts env i CONV t t');
-		   (fun i -> exact_ise_stack2 env i (evar_conv_x ts) rest sk2)]
-	      | None -> UnifFailure (evd, NotSameHead))
-	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
-            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
-	    in evar_eqappr_x ts env i pbty out1 out2
-	  in ise_try evd [f1;f2]
 
 	| _, _ ->
 	let f1 i = 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f02d7623d..7b1fee543 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -705,7 +705,8 @@ let define_pure_evar_as_product evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
-  let s = destSort evi.evar_concl in
+  let concl = whd_evar evd evi.evar_concl in
+  let s = destSort concl in
   let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
@@ -713,7 +714,7 @@ let define_pure_evar_as_product evd evk =
     let filter = Filter.extend 1 (evar_filter evi) in
       if is_prop_sort s then
        (* Impredicative product, conclusion must fall in [Prop]. *)
-        new_evar newenv evd1 evi.evar_concl ~src ~filter
+        new_evar newenv evd1 concl ~src ~filter
       else
 	let evd3, (rng, srng) =
 	  new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4761f824e..58d309997 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 * constant
+  | Proj of int * int * projection * Cst_stack.t
   | 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 * constant
+  | Proj of int * int * projection * Cst_stack.t
   | Fix of fixpoint * 'a t * Cst_stack.t
   | Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t
   | Shift of int
@@ -278,9 +278,9 @@ struct
        str "ZCase(" ++
 	 prvect_with_sep (pr_bar) pr_c br
        ++ str ")"
-    | Proj (n,m,p) ->
+    | Proj (n,m,p,cst) ->
       str "ZProj(" ++ int n ++ pr_comma () ++ int m ++
-	pr_comma () ++ pr_con p ++ str ")"
+	pr_comma () ++ pr_con (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
        str "ZFix(" ++ Termops.pr_fix Termops.print_constr f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
@@ -346,8 +346,9 @@ struct
 	if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2
 	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 && Constant.equal p p2
+      | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) ->
+	if Int.equal n1 n2 && Int.equal m1 m2 
+	  && Constant.equal (Projection.constant p) (Projection.constant p2)
 	then equal_rec s1 lft1 s2 lft2
 	else None
       | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
@@ -375,7 +376,7 @@ struct
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
       | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
-      | (Proj (n1,m1,p)::s1, Proj(n2,m2,p2)::s2) ->
+      | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) ->
 	Int.equal bal 0 && compare_rec 0 s1 s2
       | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -402,7 +403,7 @@ struct
 	aux (fold_array
 	       (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
 	       a1 a2) lft1 q1 lft2 q2
-      | Proj (n1,m1,p1) :: q1, Proj (n2,m2,p2) :: q2 ->
+      | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 ->
 	aux o lft1 q1 lft2 q2
       | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 ->
 	let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2)
@@ -418,7 +419,7 @@ struct
 
   let rec map f x = List.map (function
 			       | Update _ -> assert false
-			       | (Proj (_,_,_) | Shift _) as e -> e
+			       | (Proj (_,_,_,_) | Shift _) as e -> e
 			       | App (i,a,j) ->
 				  let le = j - i + 1 in
 				  App (0,Array.map f (Array.sub a i le), le-1)
@@ -537,7 +538,9 @@ 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 (Projection.make p true,f),s)
+  | f, (Proj (n,m,p,cst_l)::s) when refold -> 
+    zip ~refold (best_state (mkProj (p,f),s) cst_l)
+  | f, (Proj (n,m,p,_)::s) -> zip ~refold (mkProj (p,f),s)
   | _, (Update _::_) -> assert false
 end
 
@@ -837,7 +840,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
        and arg = pb.Declarations.proj_arg in
 	 match ReductionBehaviour.get (Globnames.ConstRef kn) with
 	 | None ->
-	   let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in
+	   let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
 	   let stack'', csts = whrec Cst_stack.empty stack' in
 	     if equal_stacks stack' stack'' then fold ()
 	     else stack'', csts
@@ -854,7 +857,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, kn) :: stack) in
+		 let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
 		   whrec Cst_stack.empty(* cst_l *) stack'
 	       | curr::remains -> 
 		 if curr == 0 then (* Try to reduce the record argument *)
@@ -910,7 +913,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') ->
 	  whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-	|args, (Stack.Proj (n,m,p)::s') ->
+	|args, (Stack.Proj (n,m,p,_)::s') ->
 	  whrec Cst_stack.empty (Stack.nth args (n+m), s')
 	|args, (Stack.Fix (f,s',cst_l)::s'') ->
 	  let x' = Stack.zip(x,args) in
@@ -935,7 +938,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,Projection.constant p) :: s''))
+		  whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p,cst_l) :: s''))
 	  | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with
 	    | None -> fold ()
 	    | Some (bef,arg,s''') ->
@@ -991,7 +994,7 @@ let local_whd_state_gen flags sigma =
     | 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, 
-			       Projection.constant p)
+			       p, Cst_stack.empty)
            :: stack))
 
     | Case (ci,p,d,lf) ->
@@ -1017,7 +1020,7 @@ let local_whd_state_gen flags sigma =
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') ->
 	  whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-	|args, (Stack.Proj (n,m,p) :: s') ->
+	|args, (Stack.Proj (n,m,p,_) :: s') ->
 	  whrec (Stack.nth args (n+m), s')
 	|args, (Stack.Fix (f,s',cst)::s'') ->
 	  let x' = Stack.zip(x,args) in
@@ -1465,12 +1468,12 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
 	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
 	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
-      |args, (Stack.Proj (n,m,p) :: stack'' as stack') ->
+      |args, (Stack.Proj (n,m,p,_) :: stack'' as stack') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
 	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
 	if isConstruct t_o then
-	  if Closure.is_transparent_constant ts p then
-	    whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'')
+	  if Projection.unfolded p || Closure.is_transparent_constant ts (Projection.constant p)
+	  then whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'')
 	  else (* Won't unfold *) (whd_betaiota_state sigma (t_o, stack_o@stack'),csts')
 	else s,csts'
       |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 9a9b34751..3335f0023 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 * constant
+  | Proj of int * int * projection * Cst_stack.t
   | 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/unification.ml b/pretyping/unification.ml
index 735d4b68a..f99ea9a52 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -390,7 +390,7 @@ 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, 
-			Projection.constant p) in
+			p, Cst_stack.empty) in
       s :: stk
   | None -> assert false)
 
@@ -519,9 +519,10 @@ let eta_constructor_app env f l1 term =
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
       | 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 (Projection.make p false, term)) projs in
+        let npars = mib.Declarations.mind_nparams in
+	let pars, l1' = Array.chop npars l1 in
+	let arg = Array.append pars [|term|] in
+	let l2 = Array.map (fun p -> mkApp (mkConstU (p,u), arg)) projs in
 	  l1', l2
       | _ -> assert false)
   | _ -> assert false
@@ -653,6 +654,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	     with ex when precatchable_exception ex ->
 	       reduce curenvnb pb b wt substn cM cN)
 
+	| Proj (p1,c1), Proj (p2,c2) ->
+	    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 *)
+		    let ty1 = get_type_of curenv ~lax:true sigma c1 in
+		    let ty2 = get_type_of curenv ~lax:true sigma c2 in
+		      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
+	      with ex when precatchable_exception ex ->
+	        unify_not_same_head curenvnb pb b wt substn cM cN
+	    else
+	      unify_not_same_head curenvnb pb b wt substn cM cN
+
+	| Proj (p1,c1), _ when not (Projection.unfolded p1) ->
+	  let cM' = Retyping.expand_projection curenv sigma p1 c1 [] in
+	    unirec_rec curenvnb CONV true false substn cM' cN
+
+	| _, Proj (p2,c2) when not (Projection.unfolded p2) ->
+	  let cN' = Retyping.expand_projection curenv sigma p2 c2 [] in
+	    unirec_rec curenvnb CONV true false substn cM cN'
+
 	| App (f1,l1), _ when 
 	    (isMeta f1 && use_metas_pattern_unification flags nb l1
             || use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
@@ -679,41 +707,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)
 
-	| Proj (p1,c1), Proj (p2,c2) ->
-	    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 *)
-		    let ty1 = get_type_of curenv ~lax:true sigma c1 in
-		    let ty2 = get_type_of curenv ~lax:true sigma c2 in
-		      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
-	      with ex when precatchable_exception ex ->
-	        unify_not_same_head curenvnb pb b wt substn cM cN
-	    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_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/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v
index e0075b833..d71727be5 100644
--- a/test-suite/bugs/closed/3566.v
+++ b/test-suite/bugs/closed/3566.v
@@ -18,4 +18,5 @@ Definition lift {T} : T -> Lift T := fun x => x.
 
 Goal forall x y : Type, x = y.
   intros.
-  pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''.
+  pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ 
+                                                   (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''.
diff --git a/test-suite/bugs/opened/3625.v b/test-suite/bugs/closed/3625.v
index 46a6c009e..a0f977eea 100644
--- a/test-suite/bugs/opened/3625.v
+++ b/test-suite/bugs/closed/3625.v
@@ -2,6 +2,8 @@ Set Implicit Arguments.
 Set Primitive Projections.
 Record prod A B := pair { fst : A ; snd : B }.
 
-Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
-(*  intros.
-    apply f_equal. *)
+Goal forall x y : prod Set Set, x.(@fst _ _) = y.(@fst _ _).
+ intros.
+ apply f_equal.
+ admit.
+Qed.
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/closed/3660.v
index ed8964ce1..ed8964ce1 100644
--- a/test-suite/bugs/opened/3660.v
+++ b/test-suite/bugs/closed/3660.v
diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v
new file mode 100644
index 000000000..a5b0e9347
--- /dev/null
+++ b/test-suite/bugs/closed/3666.v
@@ -0,0 +1,50 @@
+(* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
+
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
+Module NonPrim.
+  Record hProp := hp { hproptype :> Type ; isp : Set}.
+  Goal forall (A B : Type) (H_f : A -> V -> hProp) (H_g : B -> V -> hProp)
+              (C : Type) (h : C -> V) (b : B) (a : A) (c : C),
+         H_f a (h c) -> H_f a (h c) = H_g b (h c) -> H_g b (h c).
+    intros A B H_f H_g C h b a c H3 H'.
+    exact (@transport hProp (fun x => x) _ _ H' H3).
+    Undo.
+    Set Debug Unification.
+    exact (H' # H3).
+  Defined.
+End NonPrim.
+
+Module Prim.
+  Set Primitive Projections.
+  Set Universe Polymorphism.
+  Record hProp := hp { hproptype :> Type ; isp : Set}.
+  Goal forall (A B : Type) (H_f : A -> V -> hProp) (H_g : B -> V -> hProp)
+              (C : Type) (h : C -> V) (b : B) (a : A) (c : C),
+         H_f a (h c) -> H_f a (h c) = H_g b (h c) -> H_g b (h c).
+    intros A B H_f H_g C h b a c H3 H'.
+    exact (@transport hProp (fun x => x) _ _ H' H3).
+    Undo.
+    Set Debug Unification.
+    exact (H' # H3).
+    (* Toplevel input, characters 7-14:
+Error:
+In environment
+A : Type
+B : Type
+H_f : A -> V -> hProp
+H_g : B -> V -> hProp
+C : Type
+h : C -> V
+b : B
+a : A
+c : C
+H3 : H_f a (h c)
+H' : H_f a (h c) = H_g b (h c)
+Unable to unify "hproptype (H_f a (h c))" with "?T (H_f a (h c))".
+ *)
+  Defined.
+End Prim.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3667.v b/test-suite/bugs/closed/3667.v
index e0d0e4486..d2fc4d9bf 100644
--- a/test-suite/bugs/closed/3667.v
+++ b/test-suite/bugs/closed/3667.v
@@ -18,8 +18,8 @@ Definition set_cat : PreCategory.
                              (fun x y => x -> y))).
 Defined.
 Goal forall (A : PreCategory) (F : Functor A set_cat)
-            (a : A) (x : F a), x = x.
+            (a : A) (x : F a) (nt :NaturalTransformation F F), x = x.
   intros. 
-  pose (fun c d m => ap10 (commutes x c d m)).
+  pose (fun c d m => ap10 (commutes nt c d m)).
 
 
diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/opened/3461.v
index 1ca05a743..1b625e6a1 100644
--- a/test-suite/bugs/opened/3461.v
+++ b/test-suite/bugs/opened/3461.v
@@ -1,4 +1,5 @@
 Lemma foo (b : bool) :
   exists x : nat, x = x.
 Proof.
-eexists; Fail eexact (eq_refl b).
+eexists. 
+Fail eexact (eq_refl b).