coqcoq-tactic

Can I use a tactics under `coqtop -nois`?


Just like op of other question, I am redeveloping Coq.Init.Prelude under -nois for pratice.
I want to use tactics, but they are not working.

I tried Declare ML Module "ltac_plugin". but it didn't help.

Welcome to Coq v8.8 (eccf1d50b020e87b4d19d0bda43361e1e82d01b1)

Coq < Declare ML Module "ltac_plugin".
[Loading ML file ltac_plugin.cmxs ... done]

Coq < Goal forall A:Prop, forall proof:A, A.
1 subgoal

  ============================
  forall (A : Prop) (_ : A), A

Unnamed_thm < intro.
Toplevel input, characters 0-5:
> intro.
> ^^^^^
Error: Syntax error: illegal begin of vernac.

Solution

  • You also need to Set Default Proof Mode "Classic" to have access to the standard tactics. This option is currently undocumented.

    $ rlwrap coqtop -nois
    Welcome to Coq 8.8.0 (May 2018)
    
    Coq < Declare ML Module "ltac_plugin".
    [Loading ML file ltac_plugin.cmxs ... done]
    
    Coq < Set Default Proof Mode "Classic".
    
    Coq < Goal forall A:Prop, forall proof:A, A.
    1 subgoal
    
      ============================
      forall (A : Prop) (_ : A), A
    
    Unnamed_thm < intros.
    1 subgoal
    
      A : Prop
      proof : A
      ============================
      A
    
    Unnamed_thm < assumption.
    No more subgoals.
    
    Unnamed_thm < Qed.
    Unnamed_thm is defined