Commit 91961ccd authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Teach eval_match about "not".

When a mlw file contained "while not foo do", one of the VCs contained
"not not foo" as a hypothesis, due to a poor interaction between bool and
prop. This commit ensures that such hypotheses get simplified to "foo".
parent 553c4c52
......@@ -141,6 +141,8 @@ let rec eval_match kn stop env t =
t_label_copy t (match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
cs_equ env (eval env t1) (eval env t2)
| Tnot { t_node = Tapp (ls, [t1;t2]) } when ls_equal ls ps_equ ->
t_not_simp (cs_equ env (eval env t1) (eval env t2))
| Tapp (ls, [t1]) when is_projection ls ->
let t1 = eval env t1 in
let fn _env _t2 cs tl =
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment