coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "tactics written in ocaml" broken

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Fritjof <fritjof AT uni-bremen.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] "tactics written in ocaml" broken
Date: Wed, 04 Apr 2018 11:11:56 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:WsIiNBb6+YGlQ6MRA5+vHeb/LSx+4OfEezUN459isYplN5qZoM+8bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl8twjKxVrh2jpBJwzYHbb52OOfpiYq/QZ88WSXZbU8tTUSFKH4Oyb5EID+oEJetXsZLwplQNoBeiHwWsA/nvyjBVjXPy0qM61uUhEQXH3AwnAtkAtGrbrM7vLKcJTOu7zbPHzTHHb/xI1jf975XDfww7ofGNR71was/dxE8yHA3LiVWQrJbqPzKT1ukVvGib7vZgVeKyi2E8sQ1+vj+vxsIqh4LUhYwV0kjJ+Th6zYs2P9G0VlB3bN++HJdNtSyWKpF6Tt4sTm12oCo3ybwLtYS6cSUI0pgqwwTTZ+GDfoWK5B/oSfyfLi1ihH1/fbKynxay/lakyu37TsS131VHojZfntnLrHAN2ATf6smBSvRj4keswSuD2gPQ5+1eP0w4i6vWJ4Q8zrMyi5Yfq1nPEyHolEnuia+ZbEQk+uym6+T9ZbXmo4eROJFvhwDxMakihtazAeMiMggBR2Sb4/iz1KX//U3lR7VHluE5kq7AsJzDOcsborO5DBRO34Y46xe/Ci+m384CkXkGKlJFYhOHgJLzN1HAOvCrRcu41nq2kStpwP6OarP7A4nPKXbrjbHgOLxn5ktRzkw/wIYMyYhTD+QMCOKjAgn2rtOQTjI8Mgi1xK7FBc7vzcsxUGaLD6CeeIrIsFaTp7F8a9KQbZMY7W6uY8Mu4OTj2CdgyA0tOJKx1J5SU0iWW/FvIkGXe33p04URQT9MuRAxHrWz1A+yFAVLbnP3ZJoSoykhAdP0HdebAIe3j+7ZhXrpLthtfmlDT2u0PzLoeoGDCqUcOHrUJdVuwGUJ
Organization: X80 Heavy Industries

Hi f.

Fritjof
<fritjof AT uni-bremen.de>
writes:

> 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

Indeed, it looks pretty outdated, would you mind opening an issue in
Coq's bug tracker:

https://github.com/coq/coq/issues

E.

Re: [Coq-Club] "tactics written in ocaml" broken, Emilio Jesús Gallego Arias, 04/04/2018
- <Possible follow-up(s)>
- Re: [Coq-Club] "tactics written in ocaml" broken, makarius, 04/04/2018
  - Re: [Coq-Club] "tactics written in ocaml" broken, Théo Zimmermann, 04/04/2018