Slight simplification of naming of tactics in equality.ml (hopefully).

Isolating a core tactic in replace, shareable to cutrewrite.

8 files changed, 79 insertions, 58 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a3953bb968..11568bb4d3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2680,14 +2680,6 @@ the same variants as {\tt rewrite} has.
 
 \end{Variants}
 
-
-\subsection{\tt cutrewrite -> \term$_1$ = \term$_2$}
-\label{cutrewrite}
-\tacindex{cutrewrite}
-
-This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}}
-(see below).
-
 \subsection{\tt replace \term$_1$ with \term$_2$}
 \label{tactic:replace}
 \tacindex{replace \dots\ with}
@@ -2738,6 +2730,21 @@ n}| assumption || symmetry; try assumption]}.
     in the conclusion of the goal.
     The \nterm{clause} argument must not contain any \texttt{type of} nor \texttt{value of}.
 
+\item {\tt cutrewrite <- (\term$_1$ = \term$_2$)}
+%\label{cutrewrite}
+\tacindex{cutrewrite}
+
+This tactic is deprecated. It acts like {\tt replace {\term$_2$} with
+  {\term$_1$}}, or, equivalently as {\tt enough} (\term$_1$ =
+\term$_2$) {\tt as <-}.
+
+\item {\tt cutrewrite -> (\term$_1$ = \term$_2$)}
+%\label{cutrewrite}
+\tacindex{cutrewrite}
+
+This tactic is deprecated. It can be replaced by {\tt enough}
+(\term$_1$ = \term$_2$) {\tt as ->}.
+
 \end{Variants}
 
 \subsection{\tt subst \ident}
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 28017f8533..6a72c289c2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -249,7 +249,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
   If occurrences are set, use general rewrite.
 *)
 
-let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
+let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hook.make ()
 
 (* Do we have a JMeq instance on twice the same domains ? *)
 
@@ -359,7 +359,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     ((c,l) : constr with_bindings) with_evars =
   if occs != AllOccurrences then (
-    rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
+    rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
   else
     Proofview.Goal.raw_enter begin fun gl ->
       let sigma = Proofview.Goal.sigma gl in
@@ -374,7 +374,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       | None ->
 	  Proofview.tclORELSE
             begin
-	      rewrite_side_tac (Hook.get forward_general_rewrite_clause cls
+	      rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls
 				   lft2rgt occs (c,l) ~new_goals:[]) tac
             end
             begin function
@@ -413,7 +413,7 @@ 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 general_rewrite_clause l2r with_evars ?tac c cl =
   let occs_of = occurrences_map (List.fold_left
     (fun acc ->
       function ArgArg x -> x :: acc | ArgVar _ -> acc)
@@ -474,14 +474,14 @@ let apply_special_clear_request clear_flag f =
 type delayed_open_constr_with_bindings =
     env -> evar_map -> evar_map * constr with_bindings
 
-let general_multi_multi_rewrite with_evars l cl tac =
+let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.Goal.raw_enter begin fun gl ->
       let sigma = Proofview.Goal.sigma gl in
       let env = Proofview.Goal.env gl in
       let sigma,c = f env sigma in
       tclWITHHOLES with_evars
-        (general_multi_rewrite l2r with_evars ?tac c) sigma cl
+        (general_rewrite_clause l2r with_evars ?tac c) sigma cl
     end
   in
   let rec doN l2r c = function
@@ -522,14 +522,24 @@ let check_setoid cl =
     ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) &&
 	(Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences))
     cl.onhyps
-    
+
+let replace_core clause l2r eq =
+  if check_setoid clause
+  then init_setoid ();
+  tclTHENFIRST
+    (assert_as false None eq)
+    (onLastHypId (fun id ->
+      tclTHEN
+        (tclTRY (general_rewrite_clause l2r false (mkVar id,NoBindings) clause))
+	(clear [id])))
+
 (* eq,sym_eq : equality on Type and its symmetry theorem
-   c2 c1 : c1 is to be replaced by c2
+   c1 c2 : c1 is to be replaced by c2
    unsafe : If true, do not check that c1 and c2 are convertible
    tac : Used to prove the equality c1 = c2
    gl : goal *)
 
-let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
+let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let try_prove_eq =
     match try_prove_eq_opt with
       | None -> Proofview.tclUNIT ()
@@ -551,30 +561,26 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
   | Some evd ->
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
+    Tacticals.New.pf_constr_of_global sym (fun sym ->
     Tacticals.New.pf_constr_of_global e (fun e ->
     let eq = applist (e, [t1;c1;c2]) in
-    if check_setoid clause
-    then init_setoid ();
-    Tacticals.New.pf_constr_of_global sym (fun sym ->
-      tclTHENS (assert_as false None eq)
-	[onLastHypId (fun id ->
-	  tclTHEN
-	    (tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
-	    (clear [id]));
-	 tclFIRST
-	   [assumption;
-	    tclTHEN (apply sym) assumption;
-	    try_prove_eq
-	   ]
-	]))
+    tclTHENLAST
+      (replace_core clause l2r eq)
+      (tclFIRST
+         [assumption;
+          tclTHEN (apply sym) assumption;
+          try_prove_eq
+         ])))
   end
 
-let replace c2 c1 = multi_replace onConcl c2 c1 false None
+let replace c1 c2 =
+  replace_using_leibniz onConcl c2 c1 false false None
 
-let replace_by c2 c1 tac = multi_replace onConcl c2 c1 false (Some tac)
+let replace_by c1 c2 tac =
+  replace_using_leibniz onConcl c2 c1 false false (Some tac)
 
-let replace_in_clause_maybe_by c2 c1 cl tac_opt =
-  multi_replace cl c2 c1 false tac_opt
+let replace_in_clause_maybe_by c1 c2 cl tac_opt =
+  replace_using_leibniz cl c2 c1 false false tac_opt
 
 (* End of Eduardo's code. The rest of this file could be improved
    using the functions match_with_equation, etc that I defined
@@ -1597,7 +1603,6 @@ let unfold_body x =
   end
   end
 
-
 let restrict_to_eq_and_identity eq = (* compatibility *)
   if not (is_global glob_eq eq) &&
     not (is_global glob_identity eq) 
@@ -1713,7 +1718,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   subst_gen flags.rewrite_dependent_proof ids
   end
 
-(* Rewrite the first assumption for which the condition faildir does not fail
+(* Rewrite the first assumption for which a condition holds
    and gives the direction of the rewrite *)
 
 let cond_eq_term_left c t gl =
@@ -1736,14 +1741,14 @@ let cond_eq_term c t gl =
     else failwith "not convertible"
   with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
 
-let rewrite_multi_assumption_cond cond_eq_term cl =
+let rewrite_assumption_cond cond_eq_term cl =
   let rec arec hyps gl = match hyps with
     | [] -> error "No such assumption."
     | (id,_,t) ::rest ->
 	begin
 	  try
             let dir = cond_eq_term t gl in
-	    general_multi_rewrite dir false (mkVar id,NoBindings) cl
+	    general_rewrite_clause dir false (mkVar id,NoBindings) cl
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
   in
@@ -1752,17 +1757,22 @@ let rewrite_multi_assumption_cond cond_eq_term cl =
     arec hyps gl
   end
 
-let replace_multi_term dir_opt c  =
+(* Generalize "subst x" to substitution of subterm appearing as an
+   equation in the context, but not clearing the hypothesis *)
+
+let replace_term dir_opt c  =
   let cond_eq_fun =
     match dir_opt with
       | None -> cond_eq_term c
       | Some true -> cond_eq_term_left c
       | Some false -> cond_eq_term_right c
   in
-  rewrite_multi_assumption_cond cond_eq_fun
+  rewrite_assumption_cond cond_eq_fun
+
+(* Declare rewriting tactic for intro patterns "<-" and "->" *)
 
 let _ =
-  let gmr l2r with_evars tac c = general_multi_rewrite l2r with_evars tac c in
-  Hook.set Tactics.general_multi_rewrite gmr
+  let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in
+  Hook.set Tactics.general_rewrite_clause gmr
 
 let _ = Hook.set Tactics.subst_one subst_one
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 2993c8d3a4..4899cd91d5 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -41,7 +41,7 @@ val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> constr  -> unit Pro
 
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
-val general_rewrite_clause :
+val general_setoid_rewrite_clause :
   (Id.t option -> orientation -> occurrences -> constr with_bindings ->
    new_goals:constr list -> unit Proofview.tactic) Hook.t
 
@@ -57,13 +57,13 @@ val general_rewrite_in          :
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> 
   ?tac:(unit Proofview.tactic * conditions) -> Id.t -> constr -> evars_flag -> unit Proofview.tactic
 
-val general_multi_rewrite :
+val general_rewrite_clause :
   orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
 
 type delayed_open_constr_with_bindings =
     env -> evar_map -> evar_map * constr with_bindings
 
-val general_multi_multi_rewrite :
+val general_multi_rewrite :
   evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
     clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
 
@@ -114,10 +114,10 @@ val subst : Id.t list -> unit Proofview.tactic
 val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic
 
 (* Replace term *)
-(* [replace_multi_term dir_opt c cl]
+(* [replace_term dir_opt c cl]
    perfoms replacement of [c] by the first value found in context
    (according to [dir] if given to get the rewrite direction)  in the clause [cl]
 *)
-val replace_multi_term : bool option -> constr -> clause -> unit Proofview.tactic
+val replace_term : bool option -> constr -> clause -> unit Proofview.tactic
 
 val set_eq_dec_scheme_kind : mutual scheme_kind -> unit
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e50786b31b..6478607444 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -38,9 +38,9 @@ let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
     sigma1
     (Option.map Tacinterp.eval_tactic tac)
 
-let replace_multi_term dir_opt (sigma,c) cl =
+let replace_term dir_opt (sigma,c) cl =
   Tacticals.New.tclWITHHOLES false
-    (replace_multi_term dir_opt c)
+    (replace_term dir_opt c)
     sigma
     cl
 
@@ -51,17 +51,17 @@ END
 
 TACTIC EXTEND replace_term_left
   [ "replace"  "->" open_constr(c) clause(cl) ]
-  -> [ replace_multi_term (Some true) c cl ]
+  -> [ replace_term (Some true) c cl ]
 END
 
 TACTIC EXTEND replace_term_right
   [ "replace"  "<-" open_constr(c) clause(cl) ]
-  -> [ replace_multi_term (Some false) c cl ]
+  -> [ replace_term (Some false) c cl ]
 END
 
 TACTIC EXTEND replace_term
   [ "replace" open_constr(c) clause(cl) ]
-  -> [ replace_multi_term None c cl ]
+  -> [ replace_term None c cl ]
 END
 
 let induction_arg_of_quantified_hyp = function
@@ -172,6 +172,10 @@ TACTIC EXTEND dependent_rewrite
     -> [ rewriteInHyp b c id ]
 END
 
+(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to
+    "replace u with t" or "enough (t=u) as <-" and 
+    "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *)
+
 TACTIC EXTEND cut_rewrite
 | [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
 | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 29176e2df1..ca7fb7b0a8 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1968,7 +1968,7 @@ let general_s_rewrite_clause x y z w ~new_goals =
   newtactic_init_setoid () <*>
   Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals)
 
-let _ = Hook.set Equality.general_rewrite_clause general_s_rewrite_clause
+let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause
 
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a4f9ba2d78..d9963a615d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1986,7 +1986,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	  (b,m,keep,f)) l in
         let env = Proofview.Goal.env gl in
         let cl = interp_clause ist env cl in
-        Equality.general_multi_multi_rewrite ev l cl
+        Equality.general_multi_rewrite ev l cl
           (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by),
                                  Equality.Naive)
                       by)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f3a43be0bb..4ed8b51143 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1608,7 +1608,7 @@ let simplest_split = split NoBindings
 (*****************************)
 
 (* Rewriting function for rewriting one hypothesis at the time *)
-let (forward_general_multi_rewrite, general_multi_rewrite) = Hook.make ()
+let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
 
 (* Rewriting function for substitution (x=t) everywhere at the same time *)
 let (forward_subst_one, subst_one) = Hook.make ()
@@ -1663,7 +1663,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
 
 let rewrite_hyp assert_style l2r id =
   let rew_on l2r =
-    Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in
+    Hook.get forward_general_rewrite_clause l2r false (mkVar id,NoBindings) in
   let subst_on l2r x rhs =
     Hook.get forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq c =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 19ecc2f89e..53dfed2cbc 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -398,7 +398,7 @@ val admit_as_an_axiom : unit Proofview.tactic
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> tactic
 
-val general_multi_rewrite :
+val general_rewrite_clause :
   (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t
 
 val subst_one :