diff options
| -rw-r--r-- | src/Util/Tactics/UnifyAbstractReflexivity.v | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/src/Util/Tactics/UnifyAbstractReflexivity.v b/src/Util/Tactics/UnifyAbstractReflexivity.v index bc1616cf0..687518377 100644 --- a/src/Util/Tactics/UnifyAbstractReflexivity.v +++ b/src/Util/Tactics/UnifyAbstractReflexivity.v @@ -6,16 +6,19 @@ (** This is the generic tactic; from a goal [LHS = RHS], it transforms the RHS with a passed transformer, unifies the output with LHS - using the passed [unify] tactic, and then uses the passed variant of - [exact_no_check] to [abstract] a subproof of the form [eq_refl - new_rhs]. *) + using the passed [unify] tactic, and then uses the passed variant + of [exact_no_check] to [abstract] a subproof of the form [eq_refl + new_rhs]. If there is no evar in the [LHS], don't run + transformation nor unification. *) Ltac unify_transformed_rhs_abstract_tac transform_rhs unify exact_no_check := intros; clear; lazymatch goal with | [ |- ?LHS = ?RHS ] - => let RHS' := transform_rhs RHS in - unify LHS RHS'; clear; - abstract exact_no_check (eq_refl RHS') + => tryif has_evar LHS + then let RHS' := transform_rhs RHS in + unify LHS RHS'; clear; + abstract exact_no_check (eq_refl RHS') + else abstract exact_no_check (eq_refl RHS) end. Ltac idterm x := x. @@ -26,7 +29,8 @@ Ltac unify_tac x y := unify x y. (** The tactic [abstract_vm_compute_rhs_reflexivity] unifies [LHS] with the result of [vm_compute]ing [RHS], and costs two - [vm_compute]s. *) + [vm_compute]s, unless there is no evar in the [LHS], in which case + it costs only one [vm_compute]. *) Ltac unify_abstract_vm_compute_rhs_reflexivity := unify_transformed_rhs_abstract_tac eval_vm_compute_in @@ -47,12 +51,3 @@ Ltac unify_abstract_rhs_reflexivity := idterm unify_tac exact_no_check. -(** The tactic [abstract_vm_compute_rhs_no_evar_reflexivity] costs only one - [vm_compute] and proves only evar-free goals. Best when the cost - of retypechecking [RHS] is small, or at least smaller than the - cost of retypechecking [LHS]. *) -Ltac abstract_vm_compute_rhs_no_evar_reflexivity := - unify_transformed_rhs_abstract_tac - idterm - noop2 - vm_cast_no_check. |