diff options
Diffstat (limited to 'src/Language.v')
| -rw-r--r-- | src/Language.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Language.v b/src/Language.v index 2e29b4d77..eb400d704 100644 --- a/src/Language.v +++ b/src/Language.v @@ -1157,6 +1157,7 @@ Module Compilers. Notation LiteralZRange := (@Literal base.type.zrange). Definition literal {T} (v : T) := v. Definition eagerly {T} (v : T) := v. + Definition gets_inlined (real_val : bool) {T} (v : T) : bool := real_val. (** TODO: MOVE ME? *) Module Thunked. |