Hola.
Hay cosas que van cambiando en las versiones de Coq. Incluyo algunas cosas ejemplificadas, en ciertos casos, con ejercicios del práctico:
1) Para que funcione Extraction Language Haskell, hay que poner primero algo:
Require Import Coq.extraction.ExtrHaskellBasic.
Extraction Language Haskell.
Extraction "predecesor" predspec. (* por ejemplo *)
2) Para usar functional induction en el ejercicio de mirror:
Require Import FunInd.
Functional Scheme inverse_ind := Induction for inverse Sort Prop.
Lemma MirrorC2 : forall (A : Set) (t : bintree A), {t2 : bintree A | mirror A t t2}.
Proof.
intros A t.
exists (inverse A t).
functional induction inverse A t.
...
3) En vez de "Hint Constructors BEval." poner " Hint Constructors BEval : core."
4) En Ve de usar la táctica omega de la biblioteca Omega, usen la táctica lia de la biblioteca Lia.
Saludos, Carlos