The Coq mailing list

[delahaye AT jurancon.inria.fr (David Delahaye)]

    Bonjour David,

> Comment puis-je filtrer un type dépendant dans une tactique (avec Coq
> 7.0 d'Avril 2001) ?  La définition
> 
>   Tactic Definition MyTactic t :=
>     Match t With
>       [(x:?1)?2] -> ...

    Il faut utiliser une application spécifique qui permet de faire de
l'unification d'ordre 2. La syntaxe est: (?n)@[args], où ?n est une
métavariable et args les arguments de l'application. Ici, on aurait donc:

Welcome to Coq 7.0 (April 2001)

Coq < Tactic Definition MyTactic t :=
Coq <   Match t With
Coq <   | [(x:?)(?1)@[x]] -> Cut ?1==?1. (* pour voir si cela marche *)
MyTactic is defined

Coq < Goal (x:nat)x=x.
1 subgoal
  
  ============================
   (x:nat)x=x

Unnamed_thm < Match Context With
Unnamed_thm < | [|- ?1] -> MyTactic ?1.
2 subgoals
  
  ============================
   ([x:nat]x=x)==([x:nat]x=x)->(x:nat)x=x

subgoal 2 is:
 ([x:nat]x=x)==([x:nat]x=x)

    Pour les contextes, c'est pareil.

> Tactic Definition PatternDep () :=
>   Match Context With
> [...]

    Une petite remarque en passant, les Match Context's ont une arité 
implicite
(ils attendent un but en argument), ce n'est donc pas utile de les enfermer
dans une nouvelle fermeture avec (). Cela permet d'alléger les scripts.

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The Coq Project                                  <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[Computers are like air conditioners - they stop working properly when you 
open
 Windows.]