diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-06 13:42:42 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-06 13:57:32 -0500 |
| commit | 7ec5494a230388ad0715c5dba87b57d19a0eb838 (patch) | |
| tree | af1252428a2a34b65f623170fa07f0555881a1b4 /src/Specific/FancyMachine256/Core.v | |
| parent | 1d871e22bbdf011b6711d1488d975d019367b00e (diff) | |
Add support for dependent reification
Diffstat (limited to 'src/Specific/FancyMachine256/Core.v')
| -rw-r--r-- | src/Specific/FancyMachine256/Core.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v index 207237db7..eb443a8e3 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -125,7 +125,7 @@ Section reflection. Definition Inline {t} e := @InlineConstGen base_type interp_base_type op postprocess t e. End reflection. -Ltac base_reify_op op op_head ::= +Ltac base_reify_op op op_head expr ::= lazymatch op_head with | @Interface.ldi => constr:(reify_op op op_head 1 OPldi) | @Interface.shrd => constr:(reify_op op op_head 3 OPshrd) |