diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-10 15:13:12 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-11 02:08:34 -0500 |
| commit | 40de730b6a5fd77769720cd9af87047e3f557cec (patch) | |
| tree | 15de4ccdc50c817d5f194e39a970c060d8220aff | |
| parent | 1e5b0a76fadd9255a0ead47d1327c628160b01bd (diff) | |
Also unfold tuple for reification
| -rw-r--r-- | src/Compilers/Tuple.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Compilers/Tuple.v b/src/Compilers/Tuple.v index c7e062124..8e47bf012 100644 --- a/src/Compilers/Tuple.v +++ b/src/Compilers/Tuple.v @@ -80,5 +80,9 @@ Ltac unfold_flat_interp_tuple _ := => handle n | [ |- context[@flat_interp_untuple' _ _ _ ?n] ] => handle n + | [ |- context[@tuple _ _ ?n] ] + => handle n + | [ |- context[@tuple' _ _ ?n] ] + => handle n end; - cbv [flat_interp_tuple flat_interp_tuple' flat_interp_untuple flat_interp_untuple']. + cbv [flat_interp_tuple flat_interp_tuple' flat_interp_untuple flat_interp_untuple' tuple tuple']. |