• What is Ltac?
• Is there any printing command in Ltac?
• What is the syntax for let in Ltac?
• What is the syntax for pattern matching in Ltac?
• What are the semantics for match goal?
• Why can’t I use a match goal returning a tactic in a non tail-recursive position?
• How can I generate a new name?