Type error in eval tactic

[bodeveix]

The eval tactic seems to ignore the implicit parameter annotation when reconstructing terms and thus acts as if functions were prefixed by @ while they are not. The problem seems to be solved by replacing | Symb s -> P_Iden(mk(s.sym_path,s.sym_name),false)
by | Symb s -> P_Iden(mk(s.sym_path,s.sym_name),true)

in function p_term, file tactic.ml