Distinguish two kinds of nonterminating behaviors: silent divergence

and reactive divergence.  As a consequence:
- Removed the Enilinf constructor from traceinf (values of traceinf
  type are always infinite traces).
- Traces are now uniquely defined.
- Adapted proofs big step -> small step for Clight and Cminor accordingly.
- Strengthened results in driver/Complements accordingly.
- Added common/Determinism to collect generic results about
  deterministic semantics.


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

1 files changed, 6 insertions, 7 deletions

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index f466a90..83e82e1 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -18,6 +18,12 @@ Require Import Maps.
 Require Import AST.
 Require Import Op.
 Require Import Registers.
+Require Import Globalenvs.
+Require Import Values.
+Require Import Mem.
+Require Import Integers.
+Require Import Events.
+Require Import Smallstep.
 Require Import RTL.
 Require Conventions.
 
@@ -398,13 +404,6 @@ Qed.
   here, as a warm-up exercise and because some of the lemmas will be
   useful later. *)
 
-Require Import Globalenvs.
-Require Import Values.
-Require Import Mem.
-Require Import Integers.
-Require Import Events.
-Require Import Smallstep.
-
 Definition wt_regset (env: regenv) (rs: regset) : Prop :=
   forall r, Val.has_type (rs#r) (env r).