From b863b0453331e78bb03f3ba4af538a1e8de6fd48 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 27 Oct 2016 12:35:53 +0200 Subject: [PATCH] tactics: rename auto_proper => auto_equiv --- prelude/tactics.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/prelude/tactics.v b/prelude/tactics.v index 9e70ba94..c55f53d6 100644 --- a/prelude/tactics.v +++ b/prelude/tactics.v @@ -292,9 +292,9 @@ Ltac f_equiv := end. (** auto_proper solves goals of the form "f _ = f _", for any relation and any - number of arguments, by repeatedly apply f_equiv and handling trivial cases. + number of arguments, by repeatedly applying f_equiv and handling trivial cases. If it cannot solve an equality, it will leave that to the user. *) -Ltac auto_proper := +Ltac auto_equiv := (* Deal with "pointwise_relation" *) repeat lazymatch goal with | |- pointwise_relation _ _ _ _ => intros ? @@ -302,10 +302,10 @@ Ltac auto_proper := (* Normalize away equalities. *) simplify_eq; (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *) - try (f_equiv; fast_done || auto_proper). + try (f_equiv; fast_done || auto_equiv). (** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any - number of relations. All the actual work is done by f_equiv; + number of relations. All the actual work is done by auto_equiv; solve_proper just introduces the assumptions and unfolds the first head symbol. *) Ltac solve_proper := @@ -328,7 +328,7 @@ Ltac solve_proper := | |- ?R (?f _ _) (?f _ _) => unfold f | |- ?R (?f _) (?f _) => unfold f end; - solve [ auto_proper ]. + solve [ auto_equiv ]. (** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac, and then reverts them. *) -- GitLab