renommage abstractbb: Name -> PReg

4 files changed, 7 insertions, 7 deletions

diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 0bab9426..3023ad8a 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -55,18 +55,18 @@ Definition assign (m: mem) (x:R.t) (v: value): mem
   := fun y => if R.eq_dec x y then v else m y.
 
 Inductive exp :=
-  | Name (x:R.t)
+  | PReg (x:R.t)
   | Op (o:op) (le: list_exp)
   | Old (e: exp)
 with list_exp :=
   | Enil
   | Econs (e:exp) (le:list_exp)
   | LOld (le: list_exp)
-  .
+.
 
 Fixpoint exp_eval (e: exp) (m old: mem): option value :=
   match e with
-  | Name x => Some (m x)
+  | PReg x => Some (m x)
   | Op o le => 
      match list_exp_eval le m old with
      | Some lv => op_eval ge o lv
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v
index 4d5c71b3..bfe79d42 100644
--- a/mppa_k1c/abstractbb/DepTreeTheory.v
+++ b/mppa_k1c/abstractbb/DepTreeTheory.v
@@ -115,7 +115,7 @@ Hint Rewrite set_spec_eq empty_spec: dict_rw.
 
 Fixpoint exp_tree (e: exp) (d old: deps): tree :=
   match e with
-  | Name x => deps_get d x
+  | PReg x => deps_get d x
   | Op o le => Top o (list_exp_tree le d old)
   | Old e => exp_tree e old old
   end
diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v
index 3cc85fd5..a4dd12eb 100644
--- a/mppa_k1c/abstractbb/ImpDep.v
+++ b/mppa_k1c/abstractbb/ImpDep.v
@@ -171,7 +171,7 @@ Hint Resolve hdeps_get_correct: wlp.
 
 Fixpoint hexp_tree (e: exp) (d od: hdeps) (dbg: option pstring) : ?? hashV tree :=
   match e with
-  | Name x => hdeps_get d x dbg
+  | PReg x => hdeps_get d x dbg
   | Op o le =>
      DO lt <~ hlist_exp_tree le d od;; 
      hTop o lt dbg
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
index 519e7e54..d1971e57 100644
--- a/mppa_k1c/abstractbb/Parallelizability.v
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -455,7 +455,7 @@ Qed.
 
 Fixpoint exp_frame (e: exp): list R.t :=
   match e with
-  | Name x => x::nil
+  | PReg x => x::nil
   | Op o le => list_exp_frame le
   | Old e => exp_frame e
   end
@@ -637,7 +637,7 @@ Qed.
 
 Fixpoint exp_sframe (e: exp): S.t :=
   match e with
-  | Name x => S.add x S.empty
+  | PReg x => S.add x S.empty
   | Op o le => list_exp_sframe le
   | Old e => exp_sframe e
   end