diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-03 12:29:07 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-03 12:29:07 -0400 |
| commit | 999cd7ee09451493a10f8f840ef3be9e7b84e033 (patch) | |
| tree | ebaf0c4e2351acdd4536d0071c175c7e40a76bad /src/Util/Tactics | |
| parent | 7e87e2654662355dec369076a4bb7dd13900300e (diff) | |
Fix parsing issue
Diffstat (limited to 'src/Util/Tactics')
| -rw-r--r-- | src/Util/Tactics/UnifyAbstractReflexivity.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/Tactics/UnifyAbstractReflexivity.v b/src/Util/Tactics/UnifyAbstractReflexivity.v index 687518377..e3e7fc77b 100644 --- a/src/Util/Tactics/UnifyAbstractReflexivity.v +++ b/src/Util/Tactics/UnifyAbstractReflexivity.v @@ -15,10 +15,10 @@ Ltac unify_transformed_rhs_abstract_tac transform_rhs unify exact_no_check := lazymatch goal with | [ |- ?LHS = ?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) + 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. |