coq-club AT inria.fr

Subject: The Coq mailing list

List archive

constr:(ltac:(first [is_var x; exact true|exact false])).

What I don't understand is how Coq turns a tactic into a term.
Is this constr:(ltac:_) documented in the manual or is this a feature?

--
Laurent

[Coq-Club] Ltac extend, Frédéric Besson, 09/20/2016
- Re: [Coq-Club] Ltac extend, Pierre-Marie Pédrot, 09/20/2016
  - Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/21/2016
    - Re: [Coq-Club] Ltac extend, Jason Gross, 09/21/2016
      - Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Robbert Krebbers, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Laurent Thery, 09/22/2016
        Re: [Coq-Club] Ltac extend, Jason Gross, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Jonathan Leivent, 09/22/2016