William Mansky
Results
2
issues of
William Mansky
In investigating why `sep_apply` failed on a fairly simple example, I discovered that `ecareful_unify` (which `ecancel` uses to resolve evars) fails on if-then-else expressions. Example: ``` Require Import VST.floyd.seplog_tactics. Goal...
VST on Iris
10
Replaced MSL with Iris, rebuilt VeriC and Floyd on top of it.