Commit 6890dea1 authored by Andrei Paskevich's avatar Andrei Paskevich

fix a "missed negation" bug in inlining (closes #11594)

parent a1e67db1
......@@ -88,7 +88,7 @@ let fold in_goal notdeft notdeff notls d (env, task) =
decl_map (t_replace_all env) (f_replace_all env) d
in
match d.d_node with
| Dlogic [ls,Some ld] when notls ls ->
| Dlogic [ls,Some ld] when not (notls ls) ->
let vl,e = open_ls_defn ld in
let inline = match e with
| Term t when notdeft t || t_s_any ffalse (ls_equal ls) t -> false
......
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