coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How do I install and use the tactics in the coqhammer?

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How do I install and use the tactics in the coqhammer?
Date: Tue, 14 Apr 2020 07:03:12 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:hXMwXBDZgYHDD6Tuzrd9UyQJP3N1i/DPJgcQr6AfoPdwSP39o8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHERLmcAFxO+7dG4jIjs3x2frh1YfUZlBhizy8erN1KV2drQzNqs4OiIdiO68ggk/ArX1JYORRwEtjIFPVlh2658Hmr80ryDhZp/90r50Iaq79ZaltFeUFXgRjCHg84YjQjTeGTQaL4SJCAGAfkx4OCA3EqhjxGJb34HOj6rhNnRKCNMizdogaHCy45v4yGhTtiWEOPHg49jOP050ivOdguBuk4idH7cvRaYCROuB5e/qEL9gfRCxIVYBQUX4YDw==

Thanks for explaining this!

--Agnishom

On Tue 14 Apr, 2020, 01:52 Łukasz Czajka, <lukaszcz AT mimuw.edu.pl> wrote:

> I am trying to install and use coqhammer. Following the readme, I installed this with
>
> opam install coq-hammer
>
> However, while the hammer tactic works, it seems hauto or sauto does not.

These tactics are not yet available in the released version 1.1.1 in
opam. For now, you need to install from source on github to use them.
I'll make a new release with these tactics soon (in a week or two).

[Coq-Club] How do I install and use the tactics in the coqhammer?, Agnishom Chattopadhyay, 04/12/2020
- Re: [Coq-Club] How do I install and use the tactics in the coqhammer?, Łukasz Czajka, 04/12/2020
  - Re: [Coq-Club] How do I install and use the tactics in the coqhammer?, Agnishom Chattopadhyay, 04/14/2020