aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/CountLets.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-10-28 22:40:02 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-10-28 22:40:02 -0400
commitb54e6b8b55c957901cfc8a1504f9cd1b281c5cdd (patch)
tree6915248e4f23e602a7c86f9f978dfb504aaf20d1 /src/Reflection/CountLets.v
parent0fb8dfb5e3dd975801d56d5fca0dc2990422350a (diff)
Add interp_type_gen_rel_pointwise2, *_gen => *
Diffstat (limited to 'src/Reflection/CountLets.v')
-rw-r--r--src/Reflection/CountLets.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/CountLets.v b/src/Reflection/CountLets.v
index 00673ae34..927e7a168 100644
--- a/src/Reflection/CountLets.v
+++ b/src/Reflection/CountLets.v
@@ -10,7 +10,7 @@ Section language.
Local Notation flat_type := (flat_type base_type_code).
Local Notation type := (type base_type_code).
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 Expr := (@Expr base_type_code interp_base_type op).
Fixpoint count_pairs (t : flat_type) : nat