diff options
Diffstat (limited to 'kvx/ValueAOpSSA.v')
| -rw-r--r-- | kvx/ValueAOpSSA.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kvx/ValueAOpSSA.v b/kvx/ValueAOpSSA.v index e94c0fc4..9e718621 100644 --- a/kvx/ValueAOpSSA.v +++ b/kvx/ValueAOpSSA.v @@ -317,7 +317,7 @@ Variable bc: block_classification. Variable ge: genv. Hypothesis GENV: genv_match bc ge. Variable sp: block. -Hypothesis STACK: bc sp <> BCinvalid. +Hypothesis STACK: bc sp = BCstack. Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). |