diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-13 23:13:32 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-13 23:13:32 -0400 |
| commit | 1786f86c8e58c4c2a2164c969c0f18d640033f64 (patch) | |
| tree | 357bb5e9a5ae96c1e8aed61a559c7d2f06fca06b /src | |
| parent | 2b5f90c8dcaf2475dc066a593976372729460b40 (diff) | |
Fix a typo
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index ceff9283e..f14f61607 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -311,8 +311,8 @@ 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_arr P1 P2) in H + => 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_arr P1 P2) + => rewrite (@eta_match_base_type_impl P1 P2) end. Ltac rewrite_eta_match_base_type_impl := repeat rewrite_eta_match_base_type_impl_step. |