#41 Tactics wizard

[Sebastián Lacuesta]

Cada táctica Coq se puede aplicar a un objetivo de prueba que tiene cierta forma, por ejemplo SPLIT se aplica si se tiene un AND de dos expresiones y el efecto es que separa en dos objetivos de prueba independientes (uno para cada expresión).
Este requerimiento permite evaluar de antemano la forma de una expresión y poder asistir al desarrollador de las pruebas sugiriéndole qué tácticas podría llegar a aplicar.