The Coq mailing list

[Eric Brisco <eric.brisco AT gmail.com>]

Is Ltac not the necessary language to define tactics, though? I merely want to start from a blank slate as an opportunity to define what I need and learn as I go. The built in tactics depend on libraries that I do not want to be using; the existence of these tactics pollutes the namespace of tactics and prevents me from using the obvious names to define my own.

On Mon, Sep 18, 2017 at 10:18 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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