coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to not load default tactics?

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to not load default tactics?
Date: Mon, 18 Sep 2017 16:18:15 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre-marie.pedrot AT inria.fr; spf=None smtp.mailfrom=pierre-marie.pedrot AT inria.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
Ironport-phdr: 9a23:PRiAXB9vh+CfGP9uRHKM819IXTAuvvDOBiVQ1KB+2ukcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47TeVDInX2z8TNXXzy3dU8sfry0ScbuiJG80Pn38JnOaS1JgiC8aPV8NkaYtwLU4/EXjJF4J+MUwwHIr0xw+uhMwn8gcUqSkgzm64K19YRi/mJItv478NJoUKPgfq1+Q6YOX2duCHw8+MC+7UqLdgCI/HZJFzxOyhc=

On 18/09/2017 16:13, Eric Brisco wrote:
> I am trying to use Coq minimally with no Init and no tactics. I have
> found that the "-noinit" option achieves the former but I have not
> figured out how to not load tactics such as "intros". I also tried
> "-nois" but this did not help.

Prior to Coq 8.7, there is no way to unplug basic tactics from Coq as
they are hardwired in the code. Nevertheless, you'll be delighted to
learn that starting from Coq 8.7, Ltac has been turned into a plugin and
thus is not loaded when starting Coq with the -noinit option, so that
you'll get no tactics at all.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] How to not load default tactics?, Eric Brisco, 09/18/2017
- Re: [Coq-Club] How to not load default tactics?, Pierre-Marie Pédrot, 09/18/2017
  - Re: [Coq-Club] How to not load default tactics?, Eric Brisco, 09/18/2017