The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I've done a bit of further investigation on the issue.  I now have two source trees.  There is one in which the tactics seem to be registering and one in which they are not.  I am unable to figure out what is different between the source trees.  Is there someone I can send the two source trees to for further investigation?  By the way, I am using Coq 8.5pl2.

                  - Ken

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Kenneth Roe <kendroe AT hotmail.com>
Sent: Friday, September 29, 2017 12:00 PM
To: Coq-Club
Subject: [Coq-Club] Adding ML tactic plugins

 

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