diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-13 23:17:20 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-13 23:17:20 -0400 |
| commit | a0e2a43ddba56a58673c1acffe6fd179f78255ee (patch) | |
| tree | 8d847ce3b65129e77275715605675a672927c8fe /src/Compilers | |
| parent | 1786f86c8e58c4c2a2164c969c0f18d640033f64 (diff) | |
Make rewrite_eta_match_base_type_impl a bit faster
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index f14f61607..a4f5506fe 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -310,9 +310,9 @@ Lemma eta_match_base_type_impl P1 P2 PZ T Proof. destruct T; reflexivity. Qed. Ltac rewrite_eta_match_base_type_impl_step := match goal with - | [ H : context[match ?T as T' in base_type return (@?P1 T' -> ?P2) with TZ => _ | _ => _ end] |- _ ] - => rewrite (@eta_match_base_type_impl P1 P2) in H - | [ |- context[match ?T as T' in base_type return (@?P1 T' -> ?P2) with TZ => _ | _ => _ end] ] - => rewrite (@eta_match_base_type_impl P1 P2) + | [ H : context[match ?T as T' in base_type return (@?P1 T' -> ?P2) with TZ => fun _ => ?PZ | TWord _ => fun _ => ?PZ end] |- _ ] + => rewrite (@eta_match_base_type_impl P1 P2 PZ T) in H + | [ |- context[match ?T as T' in base_type return (@?P1 T' -> ?P2) with TZ => fun _ => ?PZ | TWord _ => fun _ => ?PZ end] ] + => rewrite (@eta_match_base_type_impl P1 P2 PZ T) end. Ltac rewrite_eta_match_base_type_impl := repeat rewrite_eta_match_base_type_impl_step. |