diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-06 01:24:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-06 01:24:55 -0400 |
| commit | b0bbd306083ca502255e6fde01679dc7b8d4f9a2 (patch) | |
| tree | f74e76ec997600d605c7b6c5234d00f1ba036386 /src/Util/Tactics | |
| parent | ccbacc7dcbe2ab03d13245bb3c8455fa78e18a29 (diff) | |
More vigorous clearing in unify_transformed_rhs_abstract_tac
It makes more evars go away, which were giving [abstract] trouble
Diffstat (limited to 'src/Util/Tactics')
| -rw-r--r-- | src/Util/Tactics/UnifyAbstractReflexivity.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Util/Tactics/UnifyAbstractReflexivity.v b/src/Util/Tactics/UnifyAbstractReflexivity.v index e3e7fc77b..28dc942ef 100644 --- a/src/Util/Tactics/UnifyAbstractReflexivity.v +++ b/src/Util/Tactics/UnifyAbstractReflexivity.v @@ -1,4 +1,5 @@ (** * Various variants on [reflexivity] and [abstract reflexivity] for evars *) +Require Import Crypto.Util.Tactics.ClearAll. (** This file defines a number of different ways to solve goals of the form [LHS = RHS] where [LHS] may contain evars and [RHS] must not contain evars. Most tactics use [abstract] to reduce the load on @@ -11,7 +12,7 @@ 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; + intros; clear_all; lazymatch goal with | [ |- ?LHS = ?RHS ] => tryif has_evar LHS |