Tactic Language
* Tactic expressions can only be applied in the context of a goal. The evaluation yields either a term, an integer or a tactic. Intermediary results can be terms or integers but the final result must be a tactic which is then applied to the current goal
** http://coq.inria.fr/refman/Reference-Manual012.html
*** Pdf - http://coq.inria.fr/distrib/V8.3pl2/files/Reference-Manual.pdf

----
CategoryLanguage