aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-05 14:56:01 -0500
committerGravatar GitHub <noreply@github.com>2019-03-05 14:56:01 -0500
commit994f1f78a9fc77767125580fec674d1709071667 (patch)
treea46c6632d801240e2ea49e379b64fbe7800e5fd8
parent11912557b53b4d16d8d1685f020c5080d1746033 (diff)
Fix unfolding of pattern.base.lookup_default
-rw-r--r--src/Rewriter.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v
index 06f8d59fe..c39b2fe9f 100644
--- a/src/Rewriter.v
+++ b/src/Rewriter.v
@@ -2303,7 +2303,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y)
projT1 projT2
cpsbind cpscall cps_option_bind cpsreturn
PrimitiveProd.Primitive.fst PrimitiveProd.Primitive.snd
- pattern.type.subst_default pattern.base.subst_default
+ pattern.type.subst_default pattern.base.subst_default pattern.base.lookup_default
PositiveMap.add PositiveMap.find PositiveMap.empty
PositiveSet.rev PositiveSet.rev_append
pattern.ident.arg_types