aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/Conversions.v
diff options
context:
space:
mode:
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.