diff options
Diffstat (limited to 'src/Reflection/Inline.v')
| -rw-r--r-- | src/Reflection/Inline.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v index fac4d973f..946e84316 100644 --- a/src/Reflection/Inline.v +++ b/src/Reflection/Inline.v @@ -53,10 +53,9 @@ Section language. | Op _ _ op args => Op op (@inline_const_genf _ args) end. - Fixpoint inline_const_gen {t} (e : @expr (@exprf var) t) : @expr var t + Definition inline_const_gen {t} (e : @expr (@exprf var) t) : @expr var t := match e in Syntax.expr _ _ t return @expr var t with - | Return _ x => Return (inline_const_genf x) - | Abs _ _ f => Abs (fun x => @inline_const_gen _ (f (Var x))) + | Abs _ _ f => Abs (fun x => inline_const_genf (f (SmartVarVarf x))) end. Section with_is_const. |