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

9 files changed, 91 insertions, 73 deletions

diff --git a/CHANGES b/CHANGES
index 67ebffd36b..d8cdb1c7d6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -27,7 +27,8 @@ Tactics
   new option "Unset Tactic Evars Pattern Unification" to deactivate it.
 - New tactic "etransitivity".
 - Support of JMeq for "injection" and "discriminate".
-- New variant "subst'" of "subst" that supports JMeq.
+- Tactic "subst" now supports heterogeneous equality and equality
+  proofs that are dependent (use "simple subst" for preserving compatibility).
 - New tactic "decide lemma with hyp" for rewriting decidability lemmas
   when one knows which side is true.
 - Tactic "exists", "eexists", "destruct" and "edestruct" supports iteration
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
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0b69eebbd6..8495b623f2 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -119,7 +119,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 ~tac c)
+	    general_rewrite dir all_occurrences false ~tac c)
 	  tac_main bas))
       tclIDTAC lbas))
 
@@ -137,7 +137,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) !id cstr false gl in
+    let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) false !id cstr false gl in
     let gls = (fst gl').Evd.it in
     match gls with
        g::_ ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8496c3e82c..c5ffe72b4d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -65,6 +65,8 @@ let _ =
 
 (* Rewriting tactics *)
 
+type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+
 type orientation = bool
 
 type conditions =
@@ -176,6 +178,12 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
+type substitutive_equality_flags = {
+  rewrite_dependent_proof : bool;
+  use_K : bool;
+  with_evars : bool
+}
+
 let find_elim hdcncl lft2rgt dep cls args gl =
   let inccl = (cls = None) in
   if (hdcncl = constr_of_reference (Coqlib.glob_eq) ||
@@ -212,8 +220,8 @@ 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 gl hdcncl =
-  let dep = occur_term c (type_of_clause gl cls) in
+let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars dep_proof_ok gl hdcncl =
+  let dep = dep_proof_ok && occur_term 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
     (match lft2rgt with None -> false | Some b -> b)
@@ -235,7 +243,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 ?tac
+let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac
     ((c,l) : open_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)
@@ -249,7 +257,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ?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 gl hdcncl
+	    l with_evars dep_proof_ok gl hdcncl
       | None ->
 	  try
 	    rewrite_side_tac (!general_rewrite_clause cls
@@ -261,27 +269,27 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ?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 gl hdcncl
+		      (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars 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 ?tac (c,bl) =
-  general_rewrite_ebindings_clause None l2r occs ?tac (inj_open c,inj_ebindings bl)
+let general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,bl) =
+  general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (inj_open c,inj_ebindings bl)
 
-let general_rewrite l2r occs ?tac c =
-  general_rewrite_bindings l2r occs ?tac (c,NoBindings) false
+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_ebindings_in l2r occs ?tac id =
-  general_rewrite_ebindings_clause (Some id) l2r occs ?tac
+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_bindings_in l2r occs ?tac id (c,bl) =
-  general_rewrite_ebindings_clause (Some id) l2r occs ?tac (inj_open c,inj_ebindings bl)
+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 (inj_open c,inj_ebindings bl)
 
-let general_rewrite_in l2r occs ?tac id c =
-  general_rewrite_ebindings_clause (Some id) l2r occs ?tac (inj_open c,NoBindings)
+let general_rewrite_in l2r occs dep_proof_ok ?tac id c =
+  general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (inj_open c,NoBindings)
 
 let general_multi_rewrite l2r with_evars ?tac c cl =
   let occs_of = on_snd (List.fold_left
@@ -297,12 +305,12 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  | [] -> tclIDTAC
 	  | ((occs,id),_) :: l ->
 	    tclTHENFIRST
-	      (general_rewrite_ebindings_in l2r (occs_of occs) ?tac id c with_evars)
+	      (general_rewrite_ebindings_in l2r (occs_of occs) 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) ?tac c with_evars)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
 	   (do_hyps l)
     | None ->
 	(* Otherwise, if we are told to rewrite in all hypothesis via the
@@ -311,7 +319,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 ?tac id c with_evars)
+	     (general_rewrite_ebindings_in l2r all_occurrences true ?tac id c with_evars)
 	     (do_hyps_atleastonce l)
 	in
 	let do_hyps gl =
@@ -323,7 +331,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) ?tac c with_evars)
+	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) true ?tac c with_evars)
 	   do_hyps
 
 let general_multi_multi_rewrite with_evars l cl tac =
@@ -342,8 +350,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
-let rewriteRL = general_rewrite false all_occurrences
+let rewriteLR = general_rewrite true all_occurrences true
+let rewriteRL = general_rewrite false all_occurrences true
 
 (* Replacing tactics *)
 
@@ -1218,7 +1226,8 @@ let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls gls =
   let eq = pf_apply get_type_of gls c in
-  tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls
+  tclTHENS (cutSubstClause l2r eq cls)
+    [tclIDTAC; exact_no_check c] gls
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
 let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1275,7 +1284,7 @@ let is_eq_x gl x (id,_,c) =
   with PatternMatchingFailure ->
     ()
 
-let subst_one x gl =
+let subst_one dep_proof_ok x gl =
   let hyps = pf_hyps gl in
   let (_,xval,_) = pf_get_hyp gl x in
   (* If x has a body, simply replace x with body and clear x *)
@@ -1320,7 +1329,7 @@ let subst_one x gl =
   tclTHENLIST
     ((if need_rewrite then
       [generalize abshyps;
-       (if dir then rewriteLR else rewriteRL) (mkVar hyp);
+       general_rewrite dir all_occurrences dep_proof_ok (mkVar hyp);
        thin dephyps;
        tclMAP introtac depdecls]
     else
@@ -1328,13 +1337,27 @@ let subst_one x gl =
        tclMAP introtac depdecls]) @
      [tclTRY (clear [x;hyp])]) gl
 
-let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
+let subst_gen dep_proof_ok ids =
+  tclTHEN tclNORMEVAR (tclMAP (subst_one dep_proof_ok) ids)
 
-let subst_all ?(strict=true) gl =
+let subst = subst_gen true
+
+type subst_tactic_flags = {
+  only_leibniz : bool;
+  rewrite_dependent_proof : bool
+}
+
+let default_subst_tactic_flags () =
+  if Flags.version_strictly_greater Flags.V8_2 then
+    { only_leibniz = false; rewrite_dependent_proof = true }
+  else
+    { only_leibniz = true; rewrite_dependent_proof = false }
+
+let subst_all ?(flags=default_subst_tactic_flags ()) gl =
   let test (_,c) =
     try
       let lbeq,(_,x,y) = find_eq_data_decompose gl c in
-      if strict then restrict_to_eq_and_identity lbeq.eq;
+      if flags.only_leibniz then restrict_to_eq_and_identity lbeq.eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if eq_constr x y then failwith "caught";
       match kind_of_term x with Var x -> x | _ ->
@@ -1343,8 +1366,7 @@ let subst_all ?(strict=true) gl =
   in
   let ids = map_succeed test (pf_hyps_types gl) in
   let ids = list_uniquize ids in
-  subst ids gl
-
+  subst_gen flags.rewrite_dependent_proof ids gl
 
 (* Rewrite the first assumption for which the condition faildir does not fail
    and gives the direction of the rewrite *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e79254ce2b..bbe8f1e481 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -28,6 +28,8 @@ open Genarg
 open Ind_tables
 (*i*)
 
+type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
+
 type orientation = bool
 
 type conditions =
@@ -36,13 +38,15 @@ type conditions =
   | AllMatches (* Rewrite all matches whose side-conditions are solved *)
 
 val general_rewrite_bindings :
-  orientation -> occurrences -> ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
+  orientation -> occurrences -> dep_proof_flag ->
+  ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite :
-  orientation -> occurrences -> ?tac:(tactic * conditions) -> constr -> tactic
+  orientation -> occurrences -> dep_proof_flag ->
+  ?tac:(tactic * conditions) -> constr -> tactic
 
 (* Equivalent to [general_rewrite l2r] *)
-val rewriteLR   : ?tac:(tactic * conditions) -> constr -> tactic
-val rewriteRL   : ?tac:(tactic * conditions) -> constr  -> tactic
+val rewriteLR : ?tac:(tactic * conditions) -> constr -> tactic
+val rewriteRL : ?tac:(tactic * conditions) -> constr  -> tactic
 
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
@@ -52,12 +56,15 @@ val register_general_rewrite_clause :
 val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> open_constr option) -> unit
 
 val general_rewrite_ebindings_clause : identifier option ->
-  orientation -> occurrences -> ?tac:(tactic * conditions) -> open_constr with_bindings -> evars_flag -> tactic
+  orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
+  open_constr with_bindings -> evars_flag -> tactic
 
 val general_rewrite_bindings_in :
-  orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr with_bindings -> evars_flag -> tactic
+  orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
+  identifier -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite_in          :
-  orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic
+  orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) ->
+  identifier -> constr -> evars_flag -> tactic
 
 val general_multi_rewrite :
   orientation -> evars_flag -> ?tac:(tactic * conditions) -> open_constr with_bindings -> clause -> tactic
@@ -102,26 +109,6 @@ val rewriteInConcl : bool -> constr -> tactic
 (* Expect the proof of an equality; fails with raw internal errors *)
 val substClause : bool -> constr -> identifier option -> tactic
 
-(*
-(* [substHypInConcl l2r id] is obsolete: use [rewriteInConcl l2r (mkVar id)] *)
-val substHypInConcl : bool -> identifier -> tactic
-
-(* [substConcl] is an obsolete synonym for [cutRewriteInConcl] *)
-val substConcl : bool -> constr -> tactic
-
-(* [substHyp] is an obsolete synonym of [cutRewriteInHyp] *)
-val substHyp : bool -> types -> identifier -> tactic
-*)
-
-(* Obsolete, use [rewriteInConcl lr (mkVar id)] in concl
-              or [rewriteInHyp lr (mkVar id) (Some hyp)] in hyp
-   (which, if they fail, raise only UserError, not PatternMatchingFailure)
-   or [substClause lr (mkVar id) None]
-   or [substClause lr (mkVar id) (Some hyp)]
-[val hypSubst_LR : identifier -> clause -> tactic]
-[val hypSubst_RL : identifier -> clause -> tactic]
-*)
-
 val discriminable : env -> evar_map -> constr -> constr -> bool
 val injectable : env -> evar_map -> constr -> constr -> bool
 
@@ -129,8 +116,13 @@ val injectable : env -> evar_map -> constr -> constr -> bool
 
 val unfold_body : identifier -> tactic
 
+type subst_tactic_flags = {
+  only_leibniz : bool;
+  rewrite_dependent_proof : bool
+}
+
 val subst : identifier list -> tactic
-val subst_all : ?strict:bool -> tactic
+val subst_all : ?flags:subst_tactic_flags -> tactic
 
 (* Replace term *)
 (* [replace_multi_term dir_opt c cl]
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index b951734e36..b5d7d10d09 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -196,7 +196,7 @@ open Extraargs
 
 let rewrite_star clause orient occs c (tac : glob_tactic_expr option) =
   let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
-  general_rewrite_ebindings_clause clause orient occs ?tac:tac' (c,NoBindings) true
+  general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings) true
 
 let occurrences_of = function
   | n::_ as nl when n < 0 -> (false,List.map abs nl)
@@ -335,12 +335,14 @@ END
 
 TACTIC EXTEND subst
 | [ "subst" ne_var_list(l) ] -> [ subst l ]
-| [ "subst" ] -> [ subst_all ~strict:true] (* W/o JMeq *)
-
+| [ "subst" ] -> [ fun gl -> subst_all gl ]
 END
 
-TACTIC EXTEND subst'
-| [ "subst'" ] -> [ subst_all ~strict:false ] (* With JMeq *)
+let simple_subst_tactic_flags =
+  { only_leibniz = true; rewrite_dependent_proof = false }
+
+TACTIC EXTEND simple_subst
+| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags ]
 END
 
 open Evar_tactics
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 231a17f852..0e66c43c3b 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -850,7 +850,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
                   Auto.default_auto
 		]);
 	      Equality.general_rewrite_bindings_in true
-	                      all_occurrences
+	                      all_occurrences false
                               (List.hd !avoid)
                               ((mkVar (List.hd (List.tl !avoid))),
                                 Rawterm.NoBindings