diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-01 18:34:22 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-01 18:34:22 +0200 |
| commit | b8f03b19adda37c1c3275ef30d7fc106d3c97e44 (patch) | |
| tree | d29351a663fc05b518f5b6940242a7144c0d7165 /mppa_k1c/abstractbb/Parallelizability.v | |
| parent | 714a1fb988da03066629970325089e16dd146432 (diff) | |
| download | compcert-kvx-b8f03b19adda37c1c3275ef30d7fc106d3c97e44.tar.gz compcert-kvx-b8f03b19adda37c1c3275ef30d7fc106d3c97e44.zip | |
renommage abstractbb: Name -> PReg
Diffstat (limited to 'mppa_k1c/abstractbb/Parallelizability.v')
| -rw-r--r-- | mppa_k1c/abstractbb/Parallelizability.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 |