diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-24 12:35:55 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-24 12:35:55 +0200 |
| commit | 0e6cf8850f4963cc842f701471d82e5381662f5c (patch) | |
| tree | 870818e32b1a32b33e1997df3d956958193fb447 /kvx | |
| parent | 2a48e12f8c62e33e6a9f3c172a6fb9dfc85e887d (diff) | |
| download | compcert-kvx-0e6cf8850f4963cc842f701471d82e5381662f5c.tar.gz compcert-kvx-0e6cf8850f4963cc842f701471d82e5381662f5c.zip | |
fix phys_eq -> struct_eq
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index e46dddba..e82cca10 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -543,7 +543,7 @@ Definition hsilocal_simu_check hst1 hst2 : ?? unit := Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit := DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";; - phys_check n res "revmap_check_single: n and res are physically different". + struct_check n res "revmap_check_single: n and res are physically different". Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit := phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";; |