The Coq mailing list

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

  Il y a quelques années, Pierre Crégut du CNET avait écrit une
commande Specialize qui re-instantie d'un coup (sous la forme de
macros syntaxiques) les constructions qui avait été généralisée par la
fermeture du module où elles résidaient. Je crois que cela devrait
répondre à votre question.
 
  Je ne me souvient plus si Pierre était d'accord pour distribuer ce
code.
                                                  Hugo
 
----------------------------------------------------------------------
Exemple :
 
(* module toto.v *)
Section machine.
Variable variable : Set.
Variable domaine : variable -> Set.
Definition etat       := (V:variable) (domaine V).
Definition transition := etat -> etat.
End machine.
 
(* module titi.v *)
Section essai.
 
Variable variable : Set.
Variable domaine : variable -> Set.
 
Require Specification toto. (* Require Specification machine *)
Specialize toto "M" with variable:=variable domaine:=domaine.
 
(*
Coq < Print M__etat.
 Syntax Macro M__etat = (etat variable domaine)
Coq < Check M__etat.
(etat variable domaine)
     : Set
*)
 
End essai.