diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 10:45:44 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 10:45:44 -0400 |
| commit | 34c0849c3f22007d3587b48ad2b8809220c0320e (patch) | |
| tree | bfa489f591cbd5db00ffa0236e371e1e2f644400 /src/Assembly/Compile.v | |
| parent | d0a549c1bd43bff639748ed7ee370f70905722fd (diff) | |
Fixes for Coq 8.4
Diffstat (limited to 'src/Assembly/Compile.v')
| -rw-r--r-- | src/Assembly/Compile.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index f0ee42e7c..666cc65cc 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -209,6 +209,7 @@ Module CompileLL. | Prod t0 t1 => fun a' => match a' with | Pair _ _ a0 a1 => (vars a0) ++ (vars a1) + | _ => I (* dummy *) end end a. |