Updated compatibility for rewriting equality proofs that are dependent

- made the new "subst'" the default by renaming it "subst";
- renamed old "subst" into "simple subst";
- add option for non-rewriting of dependent proofs in general_rewrite and co
- kept use of dependent proofs in the "subst" call of "functional
  induction", in spite it introduced incompatibilities (in Compcert).

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

3 files changed, 8 insertions, 7 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e8ec962b44..e2cad94495 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1417,7 +1417,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 all_occurrences id (mkVar eq) false))
+		    (tclTRY (Equality.general_rewrite_in true all_occurrences (* dep proofs also: *) true id (mkVar eq) false))
 		    gl
 	       )
 	       eqs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e153bebf4b..2a813ae8bc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -341,7 +341,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 all_occurrences teq eq false))
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences (* deps proofs also: *) true teq eq false))
 		  (List.rev eqs);
 		(fun g1 ->
 		   let ty_teq = pf_type_of g1 (mkVar teq) in
@@ -502,6 +502,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	 in
 	 tclTHENS
 	   (general_rewrite_bindings false all_occurrences
+	      (* dep proofs also: *) true
 	      (mkVar eq,
 	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
 				dummy_loc, NamedHyp def_id, mkVar def]) false)
@@ -1185,7 +1186,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 all_occurrences
-		(mkVar heq2,
+		(* dep proofs also: *) true (mkVar heq2,
 		 ExplicitBindings[dummy_loc,NamedHyp def_id,
 				  f]) false) gls)
 	     [tclTHENLIST
@@ -1240,8 +1241,8 @@ 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 all_occurrences
-								       c_b false))
+			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences (* dep proofs also: *) true
+							       c_b false))
 			     g
 		     )
 		     [tclIDTAC;
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index c0b5542ee5..1e3765da6c 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -823,9 +823,9 @@ let raw_polynom th op lc gl =
 	      (tclTHENS
 		 (tclORELSE
                    (Equality.general_rewrite true
-		     Termops.all_occurrences c'i_eq_c''i)
+		     Termops.all_occurrences false c'i_eq_c''i)
                    (Equality.general_rewrite false
-		     Termops.all_occurrences c'i_eq_c''i))
+		     Termops.all_occurrences false c'i_eq_c''i))
                  [tac]))
 	 else
            (tclORELSE