diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-03 22:00:03 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-03 22:00:03 -0500 |
| commit | 23f642ce06af7f9141b406f5a1d23f9f62a34097 (patch) | |
| tree | d980878d7168937c681def882d1079daf55dee71 /src/Util/FixedWordSizesEquality.v | |
| parent | 1f358b2e12b3091758ba3c47df0e5688740aba4a (diff) | |
Split off non-unfolding version of fixed_size_op_to_word
Called syntactic_fixed_size_op_to_word
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 := ( |