From 23f642ce06af7f9141b406f5a1d23f9f62a34097 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 3 Feb 2017 22:00:03 -0500 Subject: Split off non-unfolding version of fixed_size_op_to_word Called syntactic_fixed_size_op_to_word --- src/Util/FixedWordSizesEquality.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'src/Util/FixedWordSizesEquality.v') 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 := ( -- cgit v1.2.3