The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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