summaryrefslogtreecommitdiff
path: root/backend/Reloadtyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Reloadtyping.v')
-rw-r--r--backend/Reloadtyping.v5
1 files changed, 1 insertions, 4 deletions
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 9f5563c..c005139 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -288,8 +288,7 @@ Proof.
rewrite loc_arguments_type; auto.
destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty.
auto 10 with reloadty.
-
- destruct (ef_reloads ef) as [] eqn:?.
+ destruct (ef_reloads ef) eqn:?.
assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence.
assert (map mreg_type (regs_for args) = map Loc.type args).
apply wt_regs_for. apply arity_ok_enough. congruence.
@@ -297,8 +296,6 @@ Proof.
auto 10 with reloadty.
auto with reloadty.
-
-
assert (map mreg_type (regs_for args) = map Loc.type args).
eauto with reloadty.
auto with reloadty.