Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for

preserving compatibility of subst after #4214 being solved.

3 files changed, 42 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 87506dadc1..85a207c29f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,11 @@ Vernacular commands
 
 - New command "Redirect" to redirect the output of a command to a file.
 
+Tactics
+
+- New flag "Set Regular Subst Tactic" which fixes "subst" in situations where
+  it failed to substitute all substitutable equations or failed to simplify
+  cycles, or accidentally unfolded local definitions (flag is off by default).
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
@@ -19,7 +24,6 @@ Tactics
 - A script using the admit tactic can no longer be concluded by either
   Qed or Defined. In the first case, Admitted can be used instead. In
   the second case, a subproof should be used.
-
 - The easy tactic and the now tactical now have a more predictable
   behavior, but they might now discharge some previously unsolved goals.
 
@@ -27,25 +31,21 @@ Extraction
 
 - Definitions extracted to Haskell GHC should no longer randomly
   segfault when some Coq types cannot be represented by Haskell types.
-
 - Definitions can now be extracted to Json for post-processing.
 
 Tools
 
 - Option -I -as has been removed, and option -R -as has been
   deprecated. In both cases, option -R can be used instead.
-
 - coq_makefile now generates double-colon rules for rules such as clean.
 
 API
 
 - The interface of [change] has changed to take a [change_arg], which
   can be built from a [constr] using [make_change_arg].
-
 - [pattern_of_constr] now returns a triplet including the cleaned-up
   [evar_map], removing the evars that were turned into metas.
 
-
 Changes from V8.4 to V8.5beta1
 ==============================
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 591fbabaef..593b7e9ea0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1662,8 +1662,21 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
+let regular_subst_tactic = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "more regular behavior of tactic subst";
+      optkey   = ["Regular";"Subst";"Tactic"];
+      optread  = (fun () -> !regular_subst_tactic);
+      optwrite = (:=) regular_subst_tactic }
+
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
+  if !regular_subst_tactic then
+
   (* First step: find hypotheses to treat in linear time *)
   let find_equations gl =
     let gl = Proofview.Goal.assume gl in
@@ -1708,6 +1721,30 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     tclMAP process ids
   end
 
+  else
+
+(* Old implementation, not able to manage configurations like a=b, a=t,
+   or situations like "a = S b, b = S a", or also accidentally unfolding
+   let-ins *)
+  Proofview.Goal.nf_enter begin fun gl ->
+  let find_eq_data_decompose = find_eq_data_decompose gl in
+  let test (_,c) =
+    try
+      let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+      let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+      if flags.only_leibniz then restrict_to_eq_and_identity eq;
+      (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+      if Term.eq_constr x y then failwith "caught";
+      match kind_of_term x with Var x -> x | _ ->
+      match kind_of_term y with Var y -> y | _ -> failwith "caught"
+    with Constr_matching.PatternMatchingFailure -> failwith "caught" in
+  let test p = try Some (test p) with Failure _ -> None in
+  let hyps = pf_hyps_types gl in
+  let ids = List.map_filter test hyps in
+  let ids = List.uniquize ids in
+  subst_gen flags.rewrite_dependent_proof ids
+  end
+
 (* Rewrite the first assumption for which a condition holds
    and gives the direction of the rewrite *)
 
diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/opened/4214.v
index cd53c898e9..cd53c898e9 100644
--- a/test-suite/bugs/closed/4214.v
+++ b/test-suite/bugs/opened/4214.v