The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Didn't work.

Does someone have a sample project that uses "VERNAC COMMAND EXTEND" (and also "TACTIC EXTEND" or what ever it became) for Coq 8.7?

            - Ken

---

From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
Sent: Saturday, November 4, 2017 1:04 AM
To: Kenneth Roe
Cc: Coq-Club
Subject: Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7

 

Hi, try adding an "open Stdarg". Best. Hugo

On Sat, Nov 04, 2017 at 03:57:20AM +0000, Kenneth Roe wrote:
> I am in the process of converting an ML plugin to Coq 8.7.  I have the
> following construct to declare some commands (inside a .ml4 file):
>
>
> VERNAC COMMAND EXTEND AR
>
> | [ "printAST" constr(def) ] -> [ Stuff.print_ast 0 def ]
>
> | [ "printExp" constr(def) ] -> [ Stuff.print_exp 0 def ]
>
> | [ "printAST" constr(def) "with" "depth" integer(depth)] -> [ Stuff.print_ast
> depth def ]
>
> END
>
>
> When I compile, I get the following error:
>
>
> File "src/plugin.ml4", line 1511, characters 2-57:
>
> Error: Unbound value wit_constr
>
>
> How do I correct this error?
>
>                    - Ken