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 --- backend/Bounds.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backend/Bounds.v') diff --git a/backend/Bounds.v b/backend/Bounds.v index d1ed28d..8c5f536 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -30,7 +30,7 @@ Require Import Conventions. These properties are used later to reason about the layout of the activation record. *) -Record bounds : Set := mkbounds { +Record bounds : Type := mkbounds { bound_int_local: Z; bound_float_local: Z; bound_int_callee_save: Z; @@ -116,7 +116,7 @@ Definition slots_of_instr (i: instruction) : list slot := | _ => nil end. -Definition max_over_list (A: Set) (valu: A -> Z) (l: list A) : Z := +Definition max_over_list (A: Type) (valu: A -> Z) (l: list A) : Z := List.fold_left (fun m l => Zmax m (valu l)) l 0. Definition max_over_instrs (valu: instruction -> Z) : Z := @@ -151,7 +151,7 @@ Definition outgoing_space (i: instruction) := match i with Lcall sig _ => size_arguments sig | _ => 0 end. Lemma max_over_list_pos: - forall (A: Set) (valu: A -> Z) (l: list A), + forall (A: Type) (valu: A -> Z) (l: list A), max_over_list A valu l >= 0. Proof. intros until valu. unfold max_over_list. @@ -196,7 +196,7 @@ Qed. (** We now show the correctness of the inferred bounds. *) Lemma max_over_list_bound: - forall (A: Set) (valu: A -> Z) (l: list A) (x: A), + forall (A: Type) (valu: A -> Z) (l: list A) (x: A), In x l -> valu x <= max_over_list A valu l. Proof. intros until x. unfold max_over_list. -- cgit v1.2.3