aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/Conversions.v
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@google.com>2016-10-14 15:51:04 -0700
committerGravatar Robert Sloan <varomodt@google.com>2016-10-14 15:52:44 -0700
commitad5c28e00ca3fb89508138354ddaf2f5ba79bd0b (patch)
treeee551d34092e24707a93a213ce981dcda4c41357 /src/Assembly/Conversions.v
parenteb17dcf4c1e7de88b24fcf3835a98756e5da2475 (diff)
Making sub bounds actually tight
Diffstat (limited to 'src/Assembly/Conversions.v')
-rw-r--r--src/Assembly/Conversions.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index bb2f1e6fa..705a49a5b 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -340,7 +340,6 @@ Module LLConversions.
admit.
- admit.
- simpl; unfold getUpperBoundOpt.
repeat rewrite convertArg_interp in H.