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 /arm/Constprop.v | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
| download | compcert-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.tar.gz compcert-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 'arm/Constprop.v')
| -rw-r--r-- | arm/Constprop.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/arm/Constprop.v b/arm/Constprop.v index b51d974e..5bd84b6d 100644 --- a/arm/Constprop.v +++ b/arm/Constprop.v @@ -32,7 +32,7 @@ Require Import Kildall. (** To each pseudo-register at each program point, the static analysis associates a compile-time approximation taken from the following set. *) -Inductive approx : Set := +Inductive approx : Type := | Novalue: approx (** No value possible, code is unreachable. *) | Unknown: approx (** All values are possible, no compile-time information is available. *) @@ -139,7 +139,7 @@ Definition eval_static_condition (cond: condition) (vl: list approx) := end. *) -Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Set := +Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type := | eval_static_condition_case1: forall c n1 n2, eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil) @@ -274,7 +274,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) := end. *) -Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Set := +Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type := | eval_static_operation_case1: forall v1, eval_static_operation_cases (Omove) (v1::nil) @@ -735,7 +735,7 @@ Definition cond_strength_reduction (cond: condition) (args: list reg) := end. *) -Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg), Set := +Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg), Type := | cond_strength_reduction_case1: forall c r1 r2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) @@ -886,7 +886,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := end. *) -Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg), Set := +Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg), Type := | op_strength_reduction_case1: forall r1 r2, op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil) @@ -1120,7 +1120,7 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) := end. *) -Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Set := +Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Type := | addr_strength_reduction_case1: forall r1 r2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) |