The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I have the following snippet of code in my .ml4 file:

TACTIC EXTEND AR2

| [ "arewrite" ] -> [ arewrite ]

END;;

(* PrintAST command

   The depth specifies the depth at which to unroll nested type definitions *)

VERNAC COMMAND EXTEND AR

| [ "printAST" constr(def) ] -> [ print_ast 0 def ]

| [ "printExp" constr(def) ] -> [ print_exp 0 def ]

| [ "printAST" constr(def) "with" "depth" integer(depth)] -> [ print_ast depth def ]

END;;

When I compile my plugin and run Coqtop, my "arewrite" tactic is not recognized.

Kenneths-MBP:plugin kendroe$ coqtop

Welcome to Coq 8.5pl2 (July 2017)

Coq < Require Export AdvancedRewrite.advancedRewrite.

[Loading ML file AdvancedRewritePlugin.cmxs ... done]

Coq < printAST (1+2).

(App (Definition Coq.Init.Nat.add (Fix (Functions ((Name add) 0 (Prod (Name n) (Name nat) (Prod (Name m) (Name nat) (Name nat))) (Lambda (Name n) (Name nat) (Lambda (Name m) (Name nat) (Case 0 (Lambda (Name n) (Name nat) (Name nat)) (CaseMatch (Name n)) (CaseBranches (Name m) (Lambda (Name p) (Name nat) (App (Construct (Name nat) 2) (App (Name add) (Name p) (Name m)))))))))) 0)) (App (Construct (Name nat) 2) (Construct (Name nat) 1)) (App (Construct (Name nat) 2) (App (Construct (Name nat) 2) (Construct (Name nat) 1))))

Coq < Theorem x: 1+2=3.

1 subgoal

  

  ============================

  1 + 2 = 3

x < arewrite.

Toplevel input, characters 0-8:

> arewrite.

> ^^^^^^^^

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

x <

The "printAST" command that I declared is recognized.  However, the "arewrite" tactic is not.  What do I need to change?

                         - Ken