aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Named
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-10-31 16:28:10 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-10-31 16:28:10 -0400
commita260aa2ad6302c4dec407419664f244541d2a075 (patch)
treecbc88ce9f1dc41f19693787559247bbba1e2b8e4 /src/Reflection/Named
parentc6e8be8aa95d3fd6ca33e187ff9f5390bb574400 (diff)
Add [f] to things that use [exprf] or [flat_type]
Diffstat (limited to 'src/Reflection/Named')
-rw-r--r--src/Reflection/Named/EstablishLiveness.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v
index b9d283013..b2be2d19b 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Reflection/Named/EstablishLiveness.v
@@ -62,7 +62,7 @@ Section language.
| LetIn tx n ex _ eC
=> let lx := @compute_livenessf ctx _ ex prefix in
let lx := merge_liveness lx (prefix ++ repeat live (count_pairs tx)) in
- let ctx := extend ctx n (SmartVal _ (fun _ => lx) tx) in
+ let ctx := extend ctx n (SmartValf _ (fun _ => lx) tx) in
@compute_livenessf ctx _ eC (prefix ++ repeat dead (count_pairs tx))
| Pair _ ex _ ey
=> merge_liveness (@compute_livenessf ctx _ ex prefix)