Added eta-expansion in kernel, type inference and tactic unification,

governed in the latter case by a flag since (useful e.g. for setoid
rewriting which otherwise loops as it is implemented).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 167 insertions, 76 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 2b6261169..d70ce83a8 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -716,15 +716,14 @@ let strip_update_shift_app head stk =
 
 let get_nth_arg head n stk =
   assert (head.norm <> Red);
-  let rec strip_rec rstk h depth n = function
+  let rec strip_rec rstk h n = function
     | Zshift(k) as e :: s ->
-        strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
+        strip_rec (e::rstk) (lift_fconstr k h) n s
     | Zapp args::s' ->
         let q = Array.length args in
         if n >= q
         then
-          strip_rec (Zapp args::rstk)
-            {norm=h.norm;term=FApp(h,args)} depth (n-q) s'
+          strip_rec (Zapp args::rstk) {norm=h.norm;term=FApp(h,args)} (n-q) s'
         else
           let bef = Array.sub args 0 n in
           let aft = Array.sub args (n+1) (q-n-1) in
@@ -732,9 +731,9 @@ let get_nth_arg head n stk =
             List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
           (Some (stk', args.(n)), append_stack aft s')
     | Zupdate(m)::s ->
-        strip_rec rstk (update m (h.norm,h.term)) depth n s
+        strip_rec rstk (update m (h.norm,h.term)) n s
     | s -> (None, List.rev rstk @ s) in
-  strip_rec [] head 0 n stk
+  strip_rec [] head n stk
 
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
@@ -757,6 +756,12 @@ let rec get_args n tys f e stk =
           get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
+(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
+let rec eta_expand_stack = function
+  | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+      e :: eta_expand_stack s
+  | [] ->
+      [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
 
 (* Iota reduction: extract the arguments to be passed to the Case
    branches *)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 9dee80578..4e8b6d2bd 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -139,6 +139,7 @@ val stack_args_size : stack -> int
 val stack_tail : int -> stack -> stack
 val stack_nth : stack -> int -> fconstr
 val zip_term : (fconstr -> constr) -> constr -> stack -> constr
+val eta_expand_stack : stack -> stack
 
 (** To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 904a2a009..d3168a9a1 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -244,7 +244,7 @@ let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv =
 and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
   Util.check_for_interrupt ();
   (* First head reduce both terms *)
-  let rec  whd_both (t1,stk1) (t2,stk2) =
+  let rec whd_both (t1,stk1) (t2,stk2) =
     let st1' = whd_stack (snd infos) t1 stk1 in
     let st2' = whd_stack (snd infos) t2 stk2 in
     (* Now, whd_stack on term2 might have modified st1 (due to sharing),
@@ -307,20 +307,10 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
 		    | None -> raise NotConvertible) in
           eqappr cv_pb infos app1 app2 cuniv)
 
-    (* only one constant, defined var or defined rel *)
-    | (FFlex fl1, _)      ->
-        (match unfold_reference infos fl1 with
-           | Some def1 ->
-	       eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
-           | None -> raise NotConvertible)
-    | (_, FFlex fl2)      ->
-        (match unfold_reference infos fl2 with
-           | Some def2 ->
-	       eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
-           | None -> raise NotConvertible)
-
     (* other constructors *)
     | (FLambda _, FLambda _) ->
+        (* Inconsistency: we tolerate that v1, v2 contain shift and update but
+           we throw them away *)
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly "conversion was given ill-typed terms (FLambda)";
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
@@ -335,49 +325,75 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
         let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
         ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
 
+    (* Eta-expansion on the fly *)
+    | (FLambda _, _) ->
+        if v1 <> [] then
+	  anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
+	eqappr CONV infos
+	  (lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) cuniv
+    | (_, FLambda _) ->
+        if v2 <> [] then
+	  anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
+	eqappr CONV infos
+	  (el_lift lft1,(hd1,eta_expand_stack v1)) (lft2,(bd2,[])) cuniv
+
+    (* only one constant, defined var or defined rel *)
+    | (FFlex fl1, _)      ->
+        (match unfold_reference infos fl1 with
+           | Some def1 ->
+	       eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
+           | None -> raise NotConvertible)
+    | (_, FFlex fl2)      ->
+        (match unfold_reference infos fl2 with
+           | Some def2 ->
+	       eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
+           | None -> raise NotConvertible)
+
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
-     | (FInd ind1, FInd ind2) ->
-         if eq_ind ind1 ind2
-	 then
-           convert_stacks infos lft1 lft2 v1 v2 cuniv
-         else raise NotConvertible
-
-     | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
-	 if j1 = j2 && eq_ind ind1 ind2
-	 then
-           convert_stacks infos lft1 lft2 v1 v2 cuniv
-         else raise NotConvertible
-
-     | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
-	 if op1 = op2
-	 then
-	   let n = Array.length cl1 in
-           let fty1 = Array.map (mk_clos e1) tys1 in
-           let fty2 = Array.map (mk_clos e2) tys2 in
-           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
-           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-	   let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
-           let u2 =
-             convert_vect infos
-		 (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
-           convert_stacks infos lft1 lft2 v1 v2 u2
-         else raise NotConvertible
-
-     | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
-         if op1 = op2
-         then
-	   let n = Array.length cl1 in
-           let fty1 = Array.map (mk_clos e1) tys1 in
-           let fty2 = Array.map (mk_clos e2) tys2 in
-           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
-           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-           let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
-           let u2 =
-	     convert_vect infos
-		 (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
-           convert_stacks infos lft1 lft2 v1 v2 u2
-         else raise NotConvertible
+    | (FInd ind1, FInd ind2) ->
+        if eq_ind ind1 ind2
+	then
+          convert_stacks infos lft1 lft2 v1 v2 cuniv
+        else raise NotConvertible
+
+    | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
+	if j1 = j2 && eq_ind ind1 ind2
+	then
+          convert_stacks infos lft1 lft2 v1 v2 cuniv
+        else raise NotConvertible
+
+    | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
+	if op1 = op2
+	then
+	  let n = Array.length cl1 in
+          let fty1 = Array.map (mk_clos e1) tys1 in
+          let fty2 = Array.map (mk_clos e2) tys2 in
+          let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
+          let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
+	  let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
+          let u2 =
+            convert_vect infos
+	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
+          convert_stacks infos lft1 lft2 v1 v2 u2
+        else raise NotConvertible
+
+    | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
+        if op1 = op2
+        then
+	  let n = Array.length cl1 in
+          let fty1 = Array.map (mk_clos e1) tys1 in
+          let fty2 = Array.map (mk_clos e2) tys2 in
+          let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
+          let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
+          let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
+          let u2 =
+	    convert_vect infos
+	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
+          convert_stacks infos lft1 lft2 v1 v2 u2
+        else raise NotConvertible
 
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index dcc0c4e41..67bb93092 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -307,9 +307,7 @@ Section NMORPHISM.
   Notation "x == y" := (req x y).
    Add Morphism radd : radd_ext4.  exact (Radd_ext Reqe). Qed.
    Add Morphism rmul : rmul_ext4.  exact (Rmul_ext Reqe). Qed.
-   Add Morphism ropp : ropp_ext4.  exact (Ropp_ext Reqe). Qed.
-   Add Morphism rsub : rsub_ext5.  exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite Rsth Reqe ARth.
+   Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
 
  Definition gen_phiN1 x :=
   match x with
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 581cf9251..b9f964857 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -590,6 +590,21 @@ Ltac gen_srewrite Rsth Reqe ARth :=
      | progress rewrite <- (ARopp_mul_l ARth)
      | progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ].
 
+Ltac gen_srewrite_sr Rsth Reqe ARth :=
+  repeat first
+     [ gen_reflexivity Rsth
+     | progress rewrite (ARopp_zero Rsth Reqe ARth)
+     | rewrite (ARadd_0_l ARth)
+     | rewrite (ARadd_0_r Rsth ARth)
+     | rewrite (ARmul_1_l ARth)
+     | rewrite (ARmul_1_r Rsth ARth)
+     | rewrite (ARmul_0_l ARth)
+     | rewrite (ARmul_0_r Rsth ARth)
+     | rewrite (ARdistr_l ARth)
+     | rewrite (ARdistr_r Rsth Reqe ARth)
+     | rewrite (ARadd_assoc ARth)
+     | rewrite (ARmul_assoc ARth) ].
+
 Ltac gen_add_push add Rsth Reqe ARth x :=
   repeat (match goal with
   | |- context [add (add ?y x) ?z] =>
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c26e92fd2..df0fc161a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -174,6 +174,8 @@ let rec evar_conv_x env evd pbty term1 term2 =
   match ground_test with
       Some b -> (evd,b)
     | None ->
+	(* Until pattern-unification is used consistently, use nohdbeta to not
+	   destroy beta-redexes that can be used for 1st-order unification *)
         let term1 = apprec_nohdbeta env evd term1 in
         let term2 = apprec_nohdbeta env evd term2 in
         if is_undefined_evar evd term1 then
@@ -241,13 +243,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                   (fun i -> evar_conv_x env i CONV) l1 rest2);
                (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))]
           else (i,false)
-	and f4 i =
+	and f2 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f4]
+	ise_try evd [f1; f2]
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
@@ -273,13 +275,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                   (fun i -> evar_conv_x env i CONV) rest1 l2);
                (fun i -> evar_conv_x env i pbty (applist(term1,deb1)) term2)]
           else (i,false)
-	and f4 i =
+	and f2 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f4]
+	ise_try evd [f1; f2]
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f1 i =
@@ -319,6 +321,25 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in
 	ise_try evd [f1; f2; f3]
 
+    (* Eta-expansion *)
+    | Rigid c1, (Flexible _ | MaybeFlexible _) when isLambda c1 ->
+	assert (l1 = []);
+	let (na,c1,c'1) = destLambda c1 in
+        let c = nf_evar evd c1 in
+	let env' = push_rel (na,None,c) env in
+        let appr1 = evar_apprec env' evd [] c'1 in
+	let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
+	evar_eqappr_x env' evd CONV appr1 appr2
+
+    | (Flexible _ | MaybeFlexible _), Rigid c2 when isLambda c2 ->
+	assert (l2 = []);
+	let (na,c2,c'2) = destLambda c2 in
+        let c = nf_evar evd c2 in
+	let env' = push_rel (na,None,c) env in
+	let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
+        let appr2 = evar_apprec env' evd [] c'2 in
+	evar_eqappr_x env' evd CONV appr1 appr2
+
     | Flexible ev1, Rigid _ ->
 	if
 	  is_unification_pattern_evar env ev1 l1 (applist appr2) &
@@ -384,7 +405,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
             (evd,base_sort_cmp pbty s1 s2)
 
-	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] ->
+	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) ->
+	    assert (l1=[] & l2=[]);
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
@@ -464,11 +486,25 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
             else (evd,false)
 
-	| (Meta _ | Lambda _), _ -> (evd,false)
-	| _, (Meta _ | Lambda _) -> (evd,false)
-
-	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
-	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
+	(* Eta-expansion *)
+	| Lambda (na,c1,c'1), _ ->
+	    assert (l1 = []);
+            let c = nf_evar evd c1 in
+	    let env' = push_rel (na,None,c) env in
+            let appr1 = evar_apprec env' evd [] c'1 in
+	    let appr2 = (lift 1 c2, List.map (lift 1) l2 @ [mkRel 1]) in
+	    evar_eqappr_x env' evd CONV appr1 appr2
+
+	| _, Lambda (na,c2,c'2) ->
+	    assert (l2 = []);
+            let c = nf_evar evd c2 in
+	    let env' = push_rel (na,None,c) env in
+	    let appr1 = (lift 1 c1, List.map (lift 1) l1 @ [mkRel 1]) in
+            let appr2 = evar_apprec env' evd [] c'2 in
+	    evar_eqappr_x env' evd CONV appr1 appr2
+
+	| (Meta _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
+	| _, (Meta _ | Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
 
 	| (App _ | Case _ | Fix _ | CoFix _),
 	  (App _ | Case _ | Fix _ | CoFix _) -> (evd,false)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5b8fc591e..b45d23098 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -169,7 +169,8 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
-  use_evars_pattern_unification : bool
+  use_evars_pattern_unification : bool;
+  modulo_eta : bool
 }
 
 let default_unify_flags = {
@@ -178,6 +179,7 @@ let default_unify_flags = {
   modulo_delta = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  modulo_eta = true
 }
 
 let default_no_delta_unify_flags = {
@@ -186,6 +188,7 @@ let default_no_delta_unify_flags = {
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = false;
+  modulo_eta = true
 }
 
 let use_evars_pattern_unification flags =
@@ -259,6 +262,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b substn (subst1 a c) cN
 	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b substn cM (subst1 a c)
 
+        (* eta-expansion *)
+	| Lambda (na,t1,c1), _ when flags.modulo_eta ->
+	    unirec_rec (push (na,t1) curenvnb) topconv true substn
+	      c1 (mkApp (lift 1 cN,[|mkRel 1|]))
+	| _, Lambda (na,t2,c2) when flags.modulo_eta ->
+	    unirec_rec (push (na,t2) curenvnb) topconv true substn
+	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
+
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             array_fold_left2 (unirec_rec curenvnb topconv true)
 	      (unirec_rec curenvnb topconv true
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index fa34b428c..cc3040a9e 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -15,7 +15,8 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
-  use_evars_pattern_unification : bool
+  use_evars_pattern_unification : bool;
+  modulo_eta : bool
 }
 
 val default_unify_flags : unify_flags
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 85e4580c8..90c2335d6 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -107,6 +107,7 @@ let fail_quick_unif_flags = {
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = false;
+  modulo_eta = true
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 328e2d6e3..fbdf8683e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -756,6 +756,7 @@ let auto_unif_flags = {
   modulo_delta = empty_transparent_state;
   resolve_evars = true;
   use_evars_pattern_unification = false;
+  modulo_eta = true
 }
 
 (* Try unification with the precompiled clause, then use registered Apply *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 0cc39a2bb..cb52ec5b9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -96,6 +96,7 @@ let auto_unif_flags = {
   modulo_delta = var_full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  modulo_eta = true
 }
 
 let rec eq_constr_mod_evars x y =
@@ -144,7 +145,7 @@ let with_prods nprods (c, clenv) f gls =
 
 let flags_of_state st =
   {auto_unif_flags with
-    modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+    modulo_conv_on_closed_terms = Some st; modulo_delta = st; modulo_eta = false}
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a4e2b510f..281bd39bc 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -86,6 +86,7 @@ let rewrite_unif_flags = {
   Unification.modulo_delta = empty_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.modulo_eta = true
 }
 
 let side_tac tac sidetac =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 4524cf0da..f79bfa0ff 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -297,6 +297,7 @@ let rewrite_unif_flags = {
   Unification.modulo_delta = empty_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.modulo_eta = true
 }
 
 let conv_transparent_state = (Idpred.empty, Cpred.full)
@@ -307,6 +308,7 @@ let rewrite2_unif_flags = {
   Unification.modulo_delta = empty_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.modulo_eta = true
 }
 
 let setoid_rewrite_unif_flags = {
@@ -315,6 +317,7 @@ let setoid_rewrite_unif_flags = {
   Unification.modulo_delta = conv_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.modulo_eta = true
 }
 
 let convertible env evd x y =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b9cea418d..4a3001065 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -729,6 +729,7 @@ let elim_flags = {
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  modulo_eta = true
 }
 
 let elimination_clause_scheme with_evars allow_K i elimclause indclause gl =