coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Fritjof <fritjof AT uni-bremen.de>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] "tactics written in ocaml" broken
- Date: Tue, 27 Feb 2018 16:10:22 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT smtp.uni-bremen.de
- Ironport-phdr: 9a23:2CZw4BfZWCXvhHdnVCgXmhoflGMj4u6mDksu8pMizoh2WeGdxcu+Zx7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM3/mHZhNJtgqxYrx2uuwFwzIDPbYGJKPZzZL/Rcc8ASGdDWMtaSixPApm7b4sKF+cPPfxYr4jhp1sMqhu+CxSnCeThyj9Sh3/2wa860+MvEQzdwQwgGdMOvG3Po9XvKqgSVP66zK/SwTrecfxbwDHw45XGfBAmpPGDR7NwcczJxEkgFgPFklWQqZH+MD+PyusNtG2b4ux9Xuysk24qsxx9rzagy8s2l4XFmpwZxkrE+Cll2oo5OMG0RFZmbdOqH5ZcrTyWO5doTs84XW1kpSU3xqcYtZO7YSQHzoksyQTFZPydaYeI5wruVOaPLjd8g3JoYKm/hxOu8Ui40OH8S8+00FdToiVeiNnDqHUN2ALV6sSdV/Ry4F+t2TeJ1w/N9uFJOV04mKTUJpI737I8ioQfvV7DEyPqgkn6kbOael0h+uey6uTnZrvmpoWbN49xkgz+PL4ums2jAeQ6NQgOUXOW+fm61L3i5EH2W69KgeMzkqbHtpDWP9kUqbChDw9Pzokj8wq/Dyuh0NkAgXYHK0tFdAubgIjtJlHBO+v1Dey/glSpiDdk3erKPrznApXXL3jMiq3tfbhn6x0U9A1mxtdGoplQF7spIfTpW0a3usaLIAU+Nlma2ef7CtJzntcQQ2OTAKiXGL7UsBqC/O8qLu/KaIJD62W1EOQs+/O71SxxolQaZ6T8hcJGOkD9JexvJgCiWVSph94AFWkQuQ9nEb73jlzHWyReYnu0Ga4xtGhiVNCWSLzbT4Xou4SvmT+hF8QLNH1ACxWGC3rteoPCV/peMHvPcP8kqSQNUP2ac6Fk1Ryqs1WimaFiMvKS5ysZ8Jj52d144avfmENq+A==
Hi,
it looks like the article:
https://github.com/coq/coq/wiki/Tactics-Written-in-OCaml
is broken somehow.
If I follow the steps, I get:
File "plugins/hello/g_hello.ml4", line 6, characters 19-39:
Error: This expression has type
Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
but an expression was expected of type unit Proofview.tactic
Regards,
--f.
- [Coq-Club] "tactics written in ocaml" broken, Fritjof, 02/27/2018
Archive powered by MHonArc 2.6.18.