coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Eric Brisco <eric.brisco AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to not load default tactics?
Date: Mon, 18 Sep 2017 10:13:48 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=eric.brisco AT gmail.com; spf=Pass smtp.mailfrom=eric.brisco AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f181.google.com
Ironport-phdr: 9a23:n+/u6RS4t/5tTO86+SH7f9seqtpsv+yvbD5Q0YIujvd0So/mwa67bBKN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnZBUin4YAFyP6H+HpPYp8WxzeG7vZPJMD9FnD6sXbQnIQ+3pkPbrMgNioxKJaM4yx+PqXxNKMpMwmY9CEiSlF7W/Mar95krpylKuvln/dRBSq79V6s9RL1cSj8hNjZmt4XQqRDfQF7XtTMnWWIMn08QDg==

Hello,

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.

Thanks,

Eric

[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