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/Switch.v | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
| download | compcert-kvx-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.tar.gz compcert-kvx-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.zip | |
Adapted to work with Coq 8.2-1v1.4.1
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Switch.v')
| -rw-r--r-- | common/Switch.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/common/Switch.v b/common/Switch.v index 8124aea1..179d4d2e 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -23,7 +23,7 @@ Require Import Integers. (** A multi-way branch is composed of a list of (key, action) pairs, plus a default action. *) -Definition table : Set := list (int * nat). +Definition table : Type := list (int * nat). Fixpoint switch_target (n: int) (dfl: nat) (cases: table) {struct cases} : nat := @@ -37,7 +37,7 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table) Each node of the tree performs an equality test or a less-than test against one of the keys. *) -Inductive comptree : Set := +Inductive comptree : Type := | CTaction: nat -> comptree | CTifeq: int -> nat -> comptree -> comptree | CTiflt: int -> comptree -> comptree -> comptree. |