diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-20 02:49:05 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-20 02:49:05 -0400 |
| commit | d90bcfa0c4969908d3fa2fb8cb4a2bef74d6f111 (patch) | |
| tree | a445578f12158d53eeb8a546f0d7ee2a4abaa0bc /src/Specific | |
| parent | 931fe4b7d610c102a9b11209faef34212cb0f18b (diff) | |
Allow inlining expressions not returning Tbase
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Core.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/NISTP256/FancyMachine256/Core.v b/src/Specific/NISTP256/FancyMachine256/Core.v index 49d7a2b87..fec353c6f 100644 --- a/src/Specific/NISTP256/FancyMachine256/Core.v +++ b/src/Specific/NISTP256/FancyMachine256/Core.v @@ -125,7 +125,7 @@ Section reflection. | opt_noinline => no_inline e | opt_default => default_inline e | opt_inline => match t as t' return exprf _ _ t' -> inline_directive t' with - | Tbase _ => fun e => inline e + | Tbase _ => fun e => @inline _ _ _ (Tbase _) e | _ => fun e => default_inline e end e end. |