Relaxed the constraint introduced in r14190 that froze the existing

evars when rewriting. Use it for autorewrite and subst. Accept evars
instantiation in multi_rewrite so that rewrite alone remains
compatible (it is used in contribs, e.g. Godel, in places where it
does not seem absurd to allow it), but there are no good reason for
it. Comments welcome.
+ addition of some tests for rewriting (one being related to commit 14217)

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

12 files changed, 90 insertions, 55 deletions

diff --git a/CHANGES b/CHANGES
index 10b0f09cf..90d8b604f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,8 @@ Tactics
 - Unification in "apply" supports unification of patterns of the form
   ?f x y = g(x,y) (compatibility ensured by using
   "Unset Tactic Pattern Unification").
+- Tactic autorewrite does no longer instantiate pre-existing
+  existential variables (theoretical source of possible incompatibility).
 
 Vernacular commands
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bba3f95fd..1d1e4a2a6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1416,7 +1416,7 @@ let rec rewrite_eqs_in_eqs eqs =
 	       (fun id gl ->
 		  observe_tac
 		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
-		    (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* dep proofs also: *) true id (mkVar eq) false))
+		    (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* dep proofs also: *) true id (mkVar eq) false))
 		    gl
 	       )
 	       eqs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5b689625b..9b1ccde2c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -373,7 +373,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		h_intros thin_intros;
 
 		tclMAP
-		  (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* deps proofs also: *) true teq eq false))
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* deps proofs also: *) true teq eq false))
 		  (List.rev eqs);
 		(fun g1 ->
 		   let ty_teq = pf_type_of g1 (mkVar teq) in
@@ -534,7 +534,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	 in
 	 tclTHENS
 	   (general_rewrite_bindings false Termops.all_occurrences
-	      (* dep proofs also: *) true
+	      (* dep proofs also: *) true true
 	      (mkVar eq,
 	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
 				dummy_loc, NamedHyp def_id, mkVar def]) false)
@@ -1211,7 +1211,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 		  Nameops.out_name def_na
 		in
 		observe_tac "rewrite heq" (general_rewrite_bindings false Termops.all_occurrences
-		(* dep proofs also: *) true (mkVar heq2,
+		true (* dep proofs also: *) true (mkVar heq2,
 		 ExplicitBindings[dummy_loc,NamedHyp def_id,
 				  f]) false) gls)
 	     [tclTHENLIST
@@ -1266,7 +1266,7 @@ let rec introduce_all_values_eq cont_tac functional termine
 			       f_S(mkVar pmax');
 			       dummy_loc, NamedHyp def_id, f])
 			 in
-			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences (* dep proofs also: *) true
+			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences true (* dep proofs also: *) true
 							       c_b false))
 			     g
 		     )
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 7588e6a2f..89309e323 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -820,9 +820,9 @@ let raw_polynom th op lc gl =
 	      (tclTHENS
 		 (tclORELSE
                    (Equality.general_rewrite true
-		     Termops.all_occurrences false c'i_eq_c''i)
+		     Termops.all_occurrences true false c'i_eq_c''i)
                    (Equality.general_rewrite false
-		     Termops.all_occurrences false c'i_eq_c''i))
+		     Termops.all_occurrences true false c'i_eq_c''i))
                  [tac]))
 	 else
            (tclORELSE
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 55e23d342..8ccf751c4 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -117,7 +117,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
        tclTHEN tac
         (one_base (fun dir c tac ->
 	  let tac = tac, conds in
-	    general_rewrite dir all_occurrences false ~tac c)
+	    general_rewrite dir all_occurrences true false ~tac c)
 	  tac_main bas))
       tclIDTAC lbas))
 
@@ -135,7 +135,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic =
       | _ -> (* even the hypothesis id is missing *)
              error ("No such hypothesis: " ^ (string_of_id !id) ^".")
     in
-    let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) false !id cstr false gl in
+    let gl' = general_rewrite_in dir all_occurrences true ~tac:(tac, conds) false !id cstr false gl in
     let gls = gl'.Evd.it in
     match gls with
        g::_ ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3a40994f8..51265d723 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -64,6 +64,7 @@ let _ =
 (* Rewriting tactics *)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 
 type orientation = bool
 
@@ -108,12 +109,15 @@ let freeze_initial_evars sigma flags clause =
       sigma ExistentialSet.empty in
   { flags with Unification.frozen_evars = evars }
 
+let make_flags frzevars sigma flags clause =
+  if frzevars then freeze_initial_evars sigma flags clause else flags
+
 let side_tac tac sidetac =
   match sidetac with
   | None -> tac
   | Some sidetac -> tclTHENSFIRSTn tac [|tclIDTAC|] sidetac
 
-let instantiate_lemma_all env sigma gl c ty l l2r concl =
+let instantiate_lemma_all frzevars env sigma gl c ty l l2r concl =
   let eqclause = Clenv.make_clenv_binding { gl with sigma = sigma } (c,ty) l in
   let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
   let rec split_last_two = function
@@ -125,7 +129,7 @@ let instantiate_lemma_all env sigma gl c ty l l2r concl =
   let try_occ (evd', c') =
     clenv_pose_dependent_evars true {eqclause with evd = evd'}
   in
-  let flags = freeze_initial_evars sigma rewrite_unif_flags eqclause in
+  let flags = make_flags frzevars sigma rewrite_unif_flags eqclause in
   let occs =
     Unification.w_unify_to_subterm_all ~flags env
       ((if l2r then c1 else c2),concl) eqclause.evd
@@ -165,33 +169,33 @@ let rewrite_conv_closed_unif_flags = {
   Unification.allow_K_in_toplevel_higher_order_unification = false
 }
 
-let rewrite_elim with_evars c e gl =
+let rewrite_elim with_evars frzevars c e gl =
   let flags =
-    freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
+    make_flags frzevars (project gl) rewrite_conv_closed_unif_flags c in
   general_elim_clause_gen (elimination_clause_scheme with_evars ~flags) c e gl
 
-let rewrite_elim_in with_evars id c e gl =
+let rewrite_elim_in with_evars frzevars id c e gl =
   let flags =
-    freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
+    make_flags frzevars (project gl) rewrite_conv_closed_unif_flags c in
   general_elim_clause_gen
     (elimination_in_clause_scheme with_evars ~flags id) c e gl
 
 (* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause with_evars cls rew elim =
+let general_elim_clause with_evars frzevars cls rew elim =
   try
     (match cls with
       | None ->
 	  (* was tclWEAK_PROGRESS which only fails for tactics generating one
              subgoal and did not fail for useless conditional rewritings generating
              an extra condition *)
-	  tclNOTSAMEGOAL (rewrite_elim with_evars rew elim)
-      | Some id -> rewrite_elim_in with_evars id rew elim)
+	  tclNOTSAMEGOAL (rewrite_elim with_evars frzevars rew elim)
+      | Some id -> rewrite_elim_in with_evars frzevars id rew elim)
   with Pretype_errors.PretypeError (env,evd,
 				    Pretype_errors.NoOccurrenceFound (c', _)) ->
     raise (Pretype_errors.PretypeError
 	      (env,evd,Pretype_errors.NoOccurrenceFound (c', cls)))
 
-let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
+let general_elim_clause with_evars frzevars tac cls sigma c t l l2r elim gl =
   let all, firstonly, tac =
     match tac with
     | None -> false, false, None
@@ -200,12 +204,15 @@ let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
     | Some (tac, AllMatches) -> true, false, Some (tclCOMPLETE tac)
   in
   let cs =
-    (if not all then instantiate_lemma else instantiate_lemma_all)
+    (if not all then instantiate_lemma else instantiate_lemma_all frzevars)
       (pf_env gl) sigma gl c t l l2r
       (match cls with None -> pf_concl gl | Some id -> pf_get_hyp_typ gl id)
   in
   let try_clause c =
-    side_tac (tclTHEN (Refiner.tclEVARS c.evd) (general_elim_clause with_evars cls c elim)) tac
+    side_tac
+      (tclTHEN
+         (Refiner.tclEVARS c.evd)
+         (general_elim_clause with_evars frzevars cls c elim)) tac
   in
     if firstonly then
       tclFIRST (List.map try_clause cs) gl
@@ -279,12 +286,12 @@ let type_of_clause gl = function
   | None -> pf_concl gl
   | Some id -> pf_get_hyp_typ gl id
 
-let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars dep_proof_ok gl hdcncl =
+let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frzevars dep_proof_ok gl hdcncl =
   let isatomic = isProd (whd_zeta hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
   let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) gl in
-  general_elim_clause with_evars tac cls sigma c t l
+  general_elim_clause with_evars frzevars tac cls sigma c t l
     (match lft2rgt with None -> false | Some b -> b)
     {elimindex = None; elimbody = (elim,NoBindings)} gl
 
@@ -304,7 +311,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 
 (* Main function for dispatching which kind of rewriting it is about *)
 
-let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
+let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     ((c,l) : constr with_bindings) with_evars gl =
   if occs <> all_occurrences then (
     rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
@@ -317,7 +324,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t rels)
-	    l with_evars dep_proof_ok gl hdcncl
+	    l with_evars frzevars dep_proof_ok gl hdcncl
       | None ->
 	  try
 	    rewrite_side_tac (!general_rewrite_clause cls
@@ -329,27 +336,31 @@ let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
 	      | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		    leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c
-		      (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars dep_proof_ok gl hdcncl
+		      (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok gl hdcncl
 	      | None -> raise e
 		  (* error "The provided term does not end with an equality or a declared rewrite relation." *)
 
 let general_rewrite_ebindings =
   general_rewrite_ebindings_clause None
 
-let general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,bl) =
-  general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (c,bl)
+let general_rewrite_bindings l2r occs frzevars dep_proof_ok ?tac (c,bl) =
+  general_rewrite_ebindings_clause None l2r occs
+    frzevars dep_proof_ok ?tac (c,bl)
 
-let general_rewrite l2r occs dep_proof_ok ?tac c =
-  general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,NoBindings) false
+let general_rewrite l2r occs frzevars dep_proof_ok ?tac c =
+  general_rewrite_bindings l2r occs
+    frzevars dep_proof_ok ?tac (c,NoBindings) false
 
-let general_rewrite_ebindings_in l2r occs dep_proof_ok ?tac id =
-  general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac
+let general_rewrite_ebindings_in l2r occs frzevars dep_proof_ok ?tac id =
+  general_rewrite_ebindings_clause (Some id) l2r occs frzevars dep_proof_ok ?tac
 
-let general_rewrite_bindings_in l2r occs dep_proof_ok ?tac id (c,bl) =
-  general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,bl)
+let general_rewrite_bindings_in l2r occs frzevars dep_proof_ok ?tac id (c,bl) =
+  general_rewrite_ebindings_clause (Some id) l2r occs
+    frzevars dep_proof_ok ?tac (c,bl)
 
-let general_rewrite_in l2r occs dep_proof_ok ?tac id c =
-  general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,NoBindings)
+let general_rewrite_in l2r occs frzevars dep_proof_ok ?tac id c =
+  general_rewrite_ebindings_clause (Some id) l2r occs
+    frzevars dep_proof_ok ?tac (c,NoBindings)
 
 let general_multi_rewrite l2r with_evars ?tac c cl =
   let occs_of = on_snd (List.fold_left
@@ -365,12 +376,12 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  | [] -> tclIDTAC
 	  | ((occs,id),_) :: l ->
 	    tclTHENFIRST
-	      (general_rewrite_ebindings_in l2r (occs_of occs) true ?tac id c with_evars)
+	      (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
 	      (do_hyps l)
 	in
 	if cl.concl_occs = no_occurrences_expr then do_hyps l else
 	  tclTHENFIRST
-	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   (do_hyps l)
     | None ->
 	(* Otherwise, if we are told to rewrite in all hypothesis via the
@@ -379,7 +390,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  | [] -> (fun gl -> error "Nothing to rewrite.")
 	  | id :: l ->
 	    tclIFTHENTRYELSEMUST
-	     (general_rewrite_ebindings_in l2r all_occurrences true ?tac id c with_evars)
+	     (general_rewrite_ebindings_in l2r all_occurrences false true ?tac id c with_evars)
 	     (do_hyps_atleastonce l)
 	in
 	let do_hyps gl =
@@ -391,7 +402,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	in
 	if cl.concl_occs = no_occurrences_expr then do_hyps else
 	  tclIFTHENTRYELSEMUST
-	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   do_hyps
 
 type delayed_open_constr_with_bindings =
@@ -416,8 +427,8 @@ let general_multi_multi_rewrite with_evars l cl tac =
     | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
   in loop l
 
-let rewriteLR = general_rewrite true all_occurrences true
-let rewriteRL = general_rewrite false all_occurrences true
+let rewriteLR = general_rewrite true all_occurrences true true
+let rewriteRL = general_rewrite false all_occurrences true true
 
 (* Replacing tactics *)
 
@@ -1424,7 +1435,7 @@ let subst_one dep_proof_ok x gl =
   tclTHENLIST
     ((if need_rewrite then
       [generalize abshyps;
-       general_rewrite dir all_occurrences dep_proof_ok (mkVar hyp);
+       general_rewrite dir all_occurrences true dep_proof_ok (mkVar hyp);
        thin dephyps;
        tclMAP introtac depdecls]
     else
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 2cf4b3027..790594699 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -27,6 +27,7 @@ open Ind_tables
 (*i*)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 
 type orientation = bool
 
@@ -36,10 +37,10 @@ type conditions =
   | AllMatches (* Rewrite all matches whose side-conditions are solved *)
 
 val general_rewrite_bindings :
-  orientation -> occurrences -> dep_proof_flag ->
+  orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
   ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite :
-  orientation -> occurrences -> dep_proof_flag ->
+  orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
   ?tac:(tactic * conditions) -> constr -> tactic
 
 (* Equivalent to [general_rewrite l2r] *)
@@ -54,15 +55,16 @@ val register_general_rewrite_clause :
 val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit
 
 val general_rewrite_ebindings_clause : identifier option ->
-  orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
-  constr with_bindings -> evars_flag -> tactic
+  orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
+  ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
 
 val general_rewrite_bindings_in :
-  orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
+  orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
+  ?tac:(tactic * conditions) ->
   identifier -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite_in          :
-  orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
-  identifier -> constr -> evars_flag -> tactic
+  orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> 
+  ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic
 
 val general_multi_rewrite :
   orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bbeb9425e..34cb5f771 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -223,7 +223,7 @@ END
 let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
   let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
   Refiner. tclWITHHOLES false
-    (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings)) sigma true
+    (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma true
 
 let occurrences_of = function
   | n::_ as nl when n < 0 -> (false,List.map abs nl)
@@ -646,7 +646,7 @@ exception Found of tactic
 
 let rewrite_except h g =
   tclMAP (fun id -> if id = h then tclIDTAC else 
-      tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true id (mkVar h) false))
+      tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true true id (mkVar h) false))
     (Tacmach.pf_ids_of_hyps g) g
 
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
index da67d9b04..ee0920057 100644
--- a/test-suite/bugs/closed/shouldsucceed/1416.v
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -1,3 +1,8 @@
+(* In 8.1 autorewrite used to raised an anomaly here *)
+(* After resolution of the bug, autorewrite succeeded *)
+(* From forthcoming 8.4, autorewrite is forbidden to instantiate *)
+(* evars, so the new test just checks it is not an anomaly *)
+
 Set Implicit Arguments.
 
 Record Place (Env A: Type) : Type := {
@@ -22,6 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
 Proof.
   intros Env A e p; eapply ex_intro.
   autorewrite with placeeq. (* Here is the bug *)
-  auto.
-Qed.
 
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v
index 68f2f7ce7..5e9064f8a 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewrite.v
@@ -19,5 +19,11 @@ Proof.
     apply H;reflexivity.
 Qed.
 
+(* Check autorewrite does not solve existing evars *)
+(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
 
+Hint Rewrite <- plus_n_O : base1.
+Goal forall y, exists x, y+x = y.
+eexists. autorewrite with base1.
+Fail reflexivity.
 
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 3bce52fe7..3d49d3cf9 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -108,3 +108,14 @@ intros.
 rewrite (H _).
 reflexivity.
 Qed.
+
+(* Example of rewriting of a degenerated pattern using the right-most
+   argument of the goal. This is sometimes used in contribs, even if
+   ad hoc. Here, we have the extra requirement that checking types
+   needs delta-conversion *)
+
+Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p).
+Definition P := (nat * nat)%type.
+Goal forall x:P, x = x.
+intros. rewrite s.
+
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 77eeac64b..ddf5abf03 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -848,7 +848,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
                   Auto.default_auto
 		]);
 	      Equality.general_rewrite_bindings_in true
-	                      all_occurrences false
+	                      all_occurrences true false
                               (List.hd !avoid)
                               ((mkVar (List.hd (List.tl !avoid))),
                                 Glob_term.NoBindings