aboutsummaryrefslogtreecommitdiffstats
path: root/backend/ValueAnalysis.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/ValueAnalysis.v')
-rw-r--r--backend/ValueAnalysis.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 8720ce50..28934ce9 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -923,7 +923,7 @@ Proof.
rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto.
rewrite H; congruence.
}
- assert (VMTOP: forall v v', val_inject j' v v' -> vmatch bc' v Vtop).
+ assert (VMTOP: forall v v', Val.inject j' v v' -> vmatch bc' v Vtop).
{
intros. inv H; constructor. eapply PMTOP; eauto.
}