Start rewriting Ltac section
Fix compiler error