coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] How do I install and use the tactics in the coqhammer?
Date: Sun, 12 Apr 2020 10:56:59 -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:kmmfoBPVcvOM3dD+4FAl6mtUPXoX/o7sNwtQ0KIMzox0K/r/rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6msZHQy6Pg5oLMz0HJTThoK5zbOc4ZrWNixHgjumYbR3ZD62pBnNsdEfjYtzI7d5nhLGpHpTe+NT7WhtJBSalFD94JHjr9ZY7y1Mtqd5pIZ7WqLgcvFgFOEKPHEdK2kwofbTm1zDQA+IvyVOV2wXllxDBgmD5Rq8X5Gj6nKm5No44zGTOIjNdZ5xQS6rtv45Qxrpzi4McT8/ojmO255AyZlDqRfknCRRhovdYYWbLv17J/qPdtYbA2NKGMdXBXVM

Hi;

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.

I am trying to run ex1.v from here and everything up to and including line 24 works.

Line 25 fails, telling me


Syntax error: [tactic:ltac_use_default] expected after [tactic:tactic] (in [vernac:tactic_command]).

If I replace the hauto ... using ... with just hauto, I get the error message:

Error: The reference hauto was not found in the current environment.

What am I doing wrong?

--Agnishom

[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