diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-22 22:40:08 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-22 22:40:20 -0400 |
| commit | 9bd22d9031e0f5fe0dfaf47d70ab2e935ff8c712 (patch) | |
| tree | 6436a709e676aa37e1f1aea52567f7b58364eb6e /src/Assembly | |
| parent | 5aa0cf1acd464a61049fd08606e40de262164dcd (diff) | |
Fix for weaker pattern matching in < 8.4pl4
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/LL.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v index d77d9ed90..9662fcd31 100644 --- a/src/Assembly/LL.v +++ b/src/Assembly/LL.v @@ -80,6 +80,7 @@ Module LL. Definition match_arg_Prod {var t1 t2} (a:arg T var (Prod t1 t2)) : (arg T var t1 * arg T var t2) := match a with | Pair _ _ a1 a2 => (a1, a2) + | Var _ | Const _ => I (* dummy value *) end. Global Arguments match_arg_Prod / : simpl nomatch. |