Buenas.
En las instrucciones suplementarias para el práctico 6 publicadas en el foro se agrega:
"1) Para que funcione Extraction Language Haskell, hay que poner primero algo: Require Import Coq.extraction.ExtrHaskellBasic."
La parte 4 del ejercicio solicita que se defina el tipo bool para la extracción como el bool nativo de Haskell. Se entiende entonces que la parte 3 espera que el tipo bool se extraiga como el tipo bool de Coq (un enumerado con true y false).
Sin embago, parece por lo que estuve experimentando y revisando en documentación que esta importación incluye definiciones en Haskell de los tipos de Coq, por lo que se extrae un programa idéntico independientemente de si se define el tipo bool de Haskell para la extracción o no (ya que el módulo importado ya lo hace).
Por otra parte, parece que cambiando la importación por "Require Import Extraction.", se pueden extraer programas pero ya no vienen con definiciones de tipos incluidas. En ese caso sí se puede extraer primero una versión sin bool de Haskell y luego otra que sí lo utilice definiendo el tipo de extracción. ¿Sería ésta la vía a utilizar?
Si hay algún error de interpretación o en mi uso del módulo de extracción agradezco las aclaraciones.
Saludos.