diff options
Diffstat (limited to 'src/Assembly/LL.v')
| -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. |