diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
| commit | 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 (patch) | |
| tree | ec5f45b6546e19519f59b1ee0f42955616ca1b98 /common/Events.v | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
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
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/common/Events.v b/common/Events.v index c44da01..011c454 100644 --- a/common/Events.v +++ b/common/Events.v @@ -32,11 +32,11 @@ Require Import Values. allow pointers to be exchanged between the program and the outside world. *) -Inductive eventval: Set := +Inductive eventval: Type := | EVint: int -> eventval | EVfloat: float -> eventval. -Record event : Set := mkevent { +Record event : Type := mkevent { ev_name: ident; ev_args: list eventval; ev_res: eventval @@ -56,7 +56,7 @@ Definition Eextcall Definition Eapp (t1 t2: trace) : trace := t1 ++ t2. -CoInductive traceinf : Set := +CoInductive traceinf : Type := | Enilinf: traceinf | Econsinf: event -> traceinf -> traceinf. |