diff options
Diffstat (limited to 'mppa_k1c/SelectLongproof.v')
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 0700ac4d..3fa35331 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -439,6 +439,7 @@ Proof. destruct (orlimm_match a); InvEval; subst. - econstructor; split. apply eval_longconst. simpl. rewrite Int64.or_commut; auto. - TrivialExists. simpl. rewrite Val.orl_assoc. rewrite Int64.or_commut; auto. +- InvEval. TrivialExists. - TrivialExists. Qed. |