Commit 1fd7832d authored by Martin Clochard's avatar Martin Clochard

Disable (exists _. _ -> _) in case implication represent a 'by'.

parent b5bfca67
......@@ -438,6 +438,8 @@ let check_used_var t vs =
Warning.emit ?loc:vs.vs_name.id_loc "unused variable %s" s
let check_exists_implies f = match f.t_node with
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f,{ t_node = Ttrue }) },_)
when Slab.mem Term.asym_label f.t_label -> ()
| Tbinop (Timplies,_,_) -> Warning.emit ?loc:f.t_loc
"form \"exists x. P -> Q\" is likely an error (use \"not P \\/ Q\" if not)"
| _ -> ()
......
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