coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] help calling ltac1 function from ltac2

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] help calling ltac1 function from ltac2
Date: Sat, 15 Aug 2020 21:11:54 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f178.google.com
Ironport-phdr: 9a23:3cDQVxyI6Zm8LA3XCy+O+j09IxM/srCxBDY+r6Qd2ukeIJqq85mqBkHD//Il1AaPAdyFrasc06GK6ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhTexe65+IAmqoQneucQan5ZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8J+jKxVvg+vqR94zYHbfI6bO+Fzfr/fcN4AWWZMRNpdWzJHD4ihb4UPFe0BPeNAooXzpVsOqh2+BQivBOzxzj9HmGH50LY10+QkCw7G3QggE8gSv3TTqdX5OroZXOe3zKnPyzXDbvBW1in56IfWbB8suv6MXbdqfsrQzUkjDR/KjlKVqYH8OT6ey+sCvXSB4eV6SeKvl3Aoqxt3ojW3xcohhInHi5wax13K+it0w4U4K9K3RUNmYtOpEZVdui+UOoV4XM8uX29ltik6x7MJtpC2fikHxZY6yxLDa/GLbY6F6Q/tWuaWJDd3nnNleLSnihay8Umg0vb8WtO00FZNoCtIlMTHuHMV1xHL9MSLVv9w8l2i1DuPzQzf9P9ILV4umabGKZMswaY8moQSvEjfAyP7nVj6gauKeUgh9eWl6vjrbqnjq5KSOIJ0hATzP6Yhl8OlHes1NwgDX2aV+em52r3s4030TKtPg/A1nKnWrpbXLtkBqKGjGQ9ayIMj5g6/Dzi41NQYmmEKLFdfdxKGi4jlIkjOIPPlAfumjVSgjTVmyvPcMr3uBZXNKXfDkLP/crpn90Fczw8zwche55JSFL4BPOr+VlHtuNHcFBM0MAy5z/z5BNljyI8SQ3+DD62aPa/KtF+H/OMvI+2CZI8Pvzb9LuAo5/zpjX8/mF8dfrem3Z8JZ3+mBflmLECZbmDtgtcFC2sFog0+TOnyhF2YTTFTf2qyX7475jwjFI2mCp7DSpmxj7yFwSe0BYZbZntGC1CJCXfnbZ+IW/YKaCKII89uiCYIVba7S9xp6Rb7vwjjjrFjM+CcriYfrNfo0MV/z+zVjxA7szJuWZezyWaIGit2mWUJRDIy0a1Xrkl0y1PF2q99ybQMF9tV5vBEVgo3HZHZxu1+Tdv1X1SSLZ+yVF+6T4D+UnkKRdUrzopWOhovK5CZlhnGmhGSLfoNjbXSXc4796vd2z76IMMvky+XhplktEEvR450DUPjg6d+8wbJAIuQyheWkq+rceIX2yufrT7en1rLh1lRVUtLaYuAXX0bYRGI/9Hw50eHVrz3TLp+bVsHxsmFJa9HLNbuiAceSQ==

I have the following Ltac2 function to iterate over hypotheses:

Ltac2 hyploop (tac : ident -> unit) :=
let rec loop hs :=
match hs with
| h3 :: hs => match h3 with
| (h, _, _) => tac h; loop hs
end
| _ => ()
end in loop (Control.hyps ()).

How do I call hyploop from Ltac1, passing in an Ltac1 function
for the tac argument?

Ltac allhyps_fast tac :=
ltac2:(hyploop ltac1:(????)).

[Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/16/2020
- Re: [Coq-Club] help calling ltac1 function from ltac2, Tej Chajed, 08/16/2020
  - Re: [Coq-Club] help calling ltac1 function from ltac2, Jim Fehrle, 08/16/2020
  - Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/16/2020
    - Re: [Coq-Club] help calling ltac1 function from ltac2, Jason Gross, 08/16/2020
      - Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/16/2020
        
        Re: [Coq-Club] help calling ltac1 function from ltac2, Jim Fehrle, 08/16/2020
        
        Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/17/2020
        
        Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/18/2020
        Re: [Coq-Club] help calling ltac1 function from ltac2, Jason Gross, 08/18/2020
        Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/18/2020