coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about tacargs

From: scott constable <sdconsta AT syr.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Question about tacargs
Date: Sun, 3 Apr 2016 17:17:27 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
Ironport-phdr: 9a23:7O+xcxFCDB7CVeL2VIXeXZ1GYnF86YWxBRYc798ds5kLTJ75pMmwAkXT6L1XgUPTWs2DsrQf27qQ6P6rATVIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6bppdaLOk1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4HWWIKjlJDBA7e8BjwWpq55jD2ve17wzWTFdbnV/Y5VSn0vPQjcwPhlCpSb21xy2rQkMEl1K8=

In the following, why does attempt1 succeed, whereas attempt2 fails? I followed through with the Ltac debugger, and found that extractor' is never executed after intros, but I cannot come up with an explanation as to why.

Ltac my_solve m :=

intros; m.

Ltac exactor := try

match goal with

| [ H : ?P |- ?P ] => exact H

end.

Ltac exactor' :=

match goal with

| [ H : ?P |- ?P ] => exact H

| _ => idtac

end.

Theorem attempt1 : forall (A : Type) (x y : A),

x = y -> x = y.

Proof. my_solve exactor. Qed.

Theorem attempt2 : forall (A : Type) (x y : A),

x = y -> x = y.

Proof. my_solve exactor'. Qed.

Thanks in advance,

~Scott Constable

[Coq-Club] Question about tacargs, scott constable, 04/03/2016
- Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/03/2016
  - Re: [Coq-Club] Question about tacargs, scott constable, 04/04/2016
    - Re: [Coq-Club] Question about tacargs, Jonathan Leivent, 04/04/2016