From 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 26 Aug 2007 09:03:56 +0000
Subject: Ajout de common/Complements.v

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/PPC.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backend')

diff --git a/backend/PPC.v b/backend/PPC.v
index 66d96c29..5cd5e9f5 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -793,6 +793,8 @@ Inductive step: state -> trace -> state -> Prop :=
 
 End RELSEM.
 
+(** Execution of whole programs. *)
+
 Inductive initial_state (p: program): state -> Prop :=
   | initial_state_intro:
       let ge := Genv.globalenv p in
@@ -812,3 +814,4 @@ Inductive final_state: state -> int -> Prop :=
       
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+
-- 
cgit