end
in
debug t1 [t2] "PREWHD";
- let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
- let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
+ let t1' = whd ~delta:true ~subst context t1 in
+ let t2' = whd ~delta:true ~subst context t2 in
debug t1' [t2'] "POSTWHD";
aux2 test_equality_only t1' t2' ugraph
in