diff options
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 1602823f..79b9319b 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1010,7 +1010,7 @@ Lemma invert_eval_builtin_arg: /\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v /\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')). Proof. - induction 1; simpl; try (econstructor; intuition eauto with evalexpr barg; fail). + induction 1; simpl. 2-8: try (econstructor; intuition eauto with evalexpr barg; fail). - econstructor; split; eauto with evalexpr. split. constructor. auto. - econstructor; split; eauto with evalexpr. split. constructor. auto. - econstructor; split; eauto with evalexpr. split. repeat constructor. auto. |