The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

 Assume I want to program a tactic which calls "pattern (f t)",
where f is given and t has to be determined (for instance, t can be
quite big).

 Ltac funpattern f:=
   match goal with [ |-   context  [(f ?x)]] => pattern (f x) end.

Definition double (n:nat) := 2 * n.


Lemma L3 : double 0  = 0.
 funpattern double.
 simpl;auto.
Qed.

But if the argument of funpattern is not a constant, it fails :



 A call to funpattern with (plus 2) fails :

Lemma L5 : 2+3 = 1+4.
funpattern (plus 2).

User error: No matching clauses for match goal


But, the following direct call to match succeeds :
 match goal with [ |-   context  [(plus 2) ?x]] => pattern ((plus 2)  x) end.

============================
   (fun n : nat => n = 1 + 4) (2 + 3)



Does the problem comes from "match ... context" or Ltac parameter passing ?


Thank you in advance,
Pierre


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.