From bdc7b815d033f84e5538a1c8db87d3c061b1ca4c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 5 Aug 2009 14:40:34 +0000
Subject: Added 'going wrong' behaviors

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Cminorgenproof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cfrontend/Cminorgenproof.v')

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 1a68c103..984381a3 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -2610,7 +2610,7 @@ Qed.
 
 Theorem transl_program_correct:
   forall (beh: program_behavior),
-  Csharpminor.exec_program prog beh ->
+  not_wrong beh -> Csharpminor.exec_program prog beh ->
   Cminor.exec_program tprog beh.
 Proof.
   unfold Csharpminor.exec_program, Cminor.exec_program; intros.
-- 
cgit