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 --- lib/Parmov.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'lib/Parmov.v') diff --git a/lib/Parmov.v b/lib/Parmov.v index 2c7b82a7..edb267e4 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -63,7 +63,7 @@ Section PARMOV. (** The development is parameterized by the type of registers, equipped with a decidable equality. *) -Variable reg: Set. +Variable reg: Type. Variable reg_eq : forall (r1 r2: reg), {r1=r2} + {r1<>r2}. (** The [temp] function maps every register [r] to the register that @@ -93,7 +93,7 @@ Definition dests (m: moves) := List.map (@snd reg reg) m. (** The dynamic semantics of moves is given in terms of environments. An environment is a mapping of registers to their current values. *) -Variable val: Set. +Variable val: Type. Definition env := reg -> val. Lemma env_ext: @@ -186,7 +186,7 @@ Fixpoint exec_seq_rev (m: moves) (e: env) {struct m}: env := as an inductive predicate [transition] relating triples of moves, and its reflexive transitive closure [transitions]. *) -Inductive state: Set := +Inductive state: Type := State (mu: moves) (sigma: moves) (tau: moves) : state. Definition no_read (mu: moves) (d: reg) : Prop := @@ -1331,7 +1331,7 @@ Qed. Section REGISTER_CLASSES. -Variable class: Set. +Variable class: Type. Variable regclass: reg -> class. Hypothesis temp_preserves_class: forall r, regclass (temp r) = regclass r. -- cgit