aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Named/EstablishLiveness.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Reflection/Named/EstablishLiveness.v')
-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 2301eb6a1..b9d283013 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Reflection/Named/EstablishLiveness.v
@@ -37,7 +37,7 @@ Section language.
Let Tbase := @Tbase base_type_code.
Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
Local Notation interp_type := (interp_type interp_base_type).
- Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type).
+ Local Notation interp_flat_type := (interp_flat_type interp_base_type).
Local Notation exprf := (@exprf base_type_code interp_base_type op).
Local Notation expr := (@expr base_type_code interp_base_type op).