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/Switch.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'common/Switch.v') 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. -- cgit