The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Bonjour,

> J'utilisai pas mal de :
> 
>   Grammar vernac vernac : ast :=
> 
> et de 
> 
>   Grammar vernac vernac : ast :=
> 
> qui ne sont plus supportés dans la 7.4. Comment faire pour porter mes
> tactiques ? Vous trouverez un exemple de mon style de codage à cette
> huhérelle (affichage de stats pour Term.constr) :
> 
>   http://perso.wanadoo.fr/cuihtlauac.alvarado/dump-0.4.tgz

  Les grammaires tactic et vernac à base d'ast qui servent à associer
une syntaxe concrète à des tactiques ou commandes ML se font de
manière différente dans la V7.4.

  Tout se fait maintenant au niveau ML via des macros camlp4. Je
prends l'exemple de la commande "Derive Inversion_clear".

  Là où on faisait, du côté ML

let _ = 
  vinterp_add
    "MakeInversionLemmaFromHyp"
    (function
       | [VARG_NUMBER n; VARG_IDENTIFIER na; VARG_IDENTIFIER id] ->
           fun () ->
             inversion_lemma_from_goal n na id mk_Prop false inv_clear_tac
       | _ -> bad_vernac_args "MakeInversionLemmaFromHyp")

  et, du côté Coq

Grammar vernac vernac: ast :=
  der_inv_clr [ "Derive" "Inversion_clear"  identarg($na) identarg($id) "." ]
               -> [(MakeInversionLemmaFromHyp 1 $na $id)]

  il convient de faire maintenant, et uniquement au niveau ML

VERNAC COMMAND EXTEND IciUnIdentifiantUniquePourLaCommande
  [ "Derive" "Inversion_clear" ident(na) ident(id) ]
  -> [ inversion_lemma_from_goal 1 na id mk_Prop false inv_clear_tac ]
END

  Ce n'est pas encore documenté car susceptible de légères
modifications d'ici la prochaine distribution de Coq. De nombreux
exemples peuvent être trouvés dans le fichier tactics/extratactics.ml4
des sources de la 7.4. L'extension .ml4 n'est pas nécessaire (.ml
suffit) si on utilise coq_makefile car ce dernier préprocesse
systèmatiquement avec camlp4.

  Hugo