From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 5 Jun 2009 13:39:59 +0000 Subject: Adapted to work with Coq 8.2-1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Smallstep.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'common/Smallstep.v') diff --git a/common/Smallstep.v b/common/Smallstep.v index a2634be..f41fe4e 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -33,8 +33,8 @@ Set Implicit Arguments. Section CLOSURES. -Variable genv: Set. -Variable state: Set. +Variable genv: Type. +Variable state: Type. (** A one-step transition relation has the following signature. It is parameterized by a global environment, which does not @@ -197,7 +197,7 @@ Qed. (** An alternate, equivalent definition of [forever] that is useful for coinductive reasoning. *) -Variable A: Set. +Variable A: Type. Variable order: A -> A -> Prop. CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := @@ -290,7 +290,7 @@ Qed. finite prefix of this trace, or the whole trace.) *) -Inductive program_behavior: Set := +Inductive program_behavior: Type := | Terminates: trace -> int -> program_behavior | Diverges: traceinf -> program_behavior. @@ -326,8 +326,8 @@ Section SIMULATION. (** The first small-step semantics is axiomatized as follows. *) -Variable genv1: Set. -Variable state1: Set. +Variable genv1: Type. +Variable state1: Type. Variable step1: genv1 -> state1 -> trace -> state1 -> Prop. Variable initial_state1: state1 -> Prop. Variable final_state1: state1 -> int -> Prop. @@ -335,8 +335,8 @@ Variable ge1: genv1. (** The second small-step semantics is also axiomatized. *) -Variable genv2: Set. -Variable state2: Set. +Variable genv2: Type. +Variable state2: Type. Variable step2: genv2 -> state2 -> trace -> state2 -> Prop. Variable initial_state2: state2 -> Prop. Variable final_state2: state2 -> int -> Prop. -- cgit v1.2.3