Merge of the nonstrict-ops branch:

- Most RTL operators now evaluate to Some Vundef instead of None
  when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 5 insertions, 6 deletions

diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 2f96a09..50db0c6 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -629,12 +629,14 @@ Proof.
   traceEq.
   econstructor; eauto.
 
-  (* Lcond true *)
+  (* Lcond *)
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
+  destruct b.
+  (* true *)
   assert (REACH': (reachable f)!!ifso = true).
   eapply reachable_successors; eauto. simpl; auto.
-  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  exploit find_label_lin_succ; eauto. inv WTI; eauto. intros [c'' AT'].
   destruct (starts_with ifso c').
   econstructor; split.
   eapply plus_left'.  
@@ -648,10 +650,7 @@ Proof.
   econstructor; split.
   apply plus_one. eapply exec_Lcond_true; eauto.
   econstructor; eauto.
-
-  (* Lcond false *)
-  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
-  simpl in EQ. subst c.
+  (* false *)
   assert (REACH': (reachable f)!!ifnot = true).
   eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].