coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Laurent Théry <Laurent.Thery AT inria.fr>
- To: Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] No matching clauses for match
- Date: Wed, 30 Oct 2013 16:45:42 +0100
On 10/30/2013 04:01 PM, Bruno Woltzenlogel Paleo wrote:
Parameter I: Type.When you build a term I think you should add a constr:
Parameter b: I.
Parameter f: (I -> Prop) -> (I -> Prop).
Ltac tac1 H := let P := match type of H with
((f ?p) _) => p
end in cut (P b).
Ltac tac2 H := let F := match type of H with
((f ?p) ?a) => (p a)
end in cut F.
Ltac tac2 H := let F := match type of H with
((f ?p) ?a) => constr:(p a)
end in cut F.
- [Coq-Club] No matching clauses for match, Bruno Woltzenlogel Paleo, 10/30/2013
- Re: [Coq-Club] No matching clauses for match, Laurent Théry, 10/30/2013
Archive powered by MHonArc 2.6.18.