add eval tactic

[fblanqui]

Add a new tactic eval taking as argument a term that, after normalization, is interpreted as a tactic using builtins. This way, a user can define and use arbitrary functions to generate tactic expressions.
As example, see https://github.com/fblanqui/lambdapi/blob/tac/tests/OK/tactic.lp .

TODO in this PR:

• record in the sym type whether a symbol is a tactic builtin?
• find a way to handle terms and tactics taking terms as arguments
• update doc

TODO later:

• find a way to handle idents and tactics taking idents as arguments (add builtin strings #1204)
• add a builtin "function" gen_id : String -> String that generates a string prefixed by the argument which is fresh within the context where it is used (useful for tactics taking fresh identifiers as argument like assume, set, have)
• allow eval in terms and rules too?
• replace ; by and in proof scripts? problem with have

[fblanqui]

@NotBad4U your comments are welcome!

[NotBad4U]

Amazing! I will try it this week for sure.