diff options
Diffstat (limited to 'src/Util/FixedWordSizesEquality.v')
| -rw-r--r-- | src/Util/FixedWordSizesEquality.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 4dc39665c..749750625 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -215,8 +215,7 @@ Proof. wordToZ_word_case_dep_t. Qed. (** This converts goals involving (currently only binary) [wordT] operations to the corresponding goals involving [word] operations. *) -Ltac fixed_size_op_to_word := - repeat autounfold with fixed_size_constants in *; +Ltac syntactic_fixed_size_op_to_word := lazymatch goal with | [ |- context[wordToZ (word_case_dep (T:=?T) ?logsz (?wop 32) (?wop 64) (?wop 128) ?f ?x)] ] => move x at top; @@ -258,6 +257,10 @@ Ltac fixed_size_op_to_word := refine (@wordToZ_word_case_dep_quadop wop P _); intros logsz x y z w; intros end. +Ltac fixed_size_op_to_word := + repeat autounfold with fixed_size_constants in *; + syntactic_fixed_size_op_to_word. + Section Updates. Local Notation bound n lower value upper := ( |