Don't require keeping track of which goals have evars; check that in tactics

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.