coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7
Date: Sat, 4 Nov 2017 03:57:20 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BN3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:Vayn2xT0n5PzaYbHjY93Nc/H/tpsv+yvbD5Q0YIujvd0So/mwa67YhGN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnZBUin4YCFyP6HeHpPYx5C80Pn38JnOaS1JgiC8aPV8NkPlgx/Ws5w1jI1kJ7oxgiHOrzMceOlQyXlvKHqTmAr578a0upVk9nID6Loa68dcXPCiLOwDRrtCAWF+Pg==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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

[Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
- Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Hugo Herbelin, 11/04/2017
  - Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
    - Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Matej Košík, 11/04/2017
      - Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
        
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Maxime Dénès, 11/04/2017
        
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
        
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Matej Košík, 11/04/2017
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/04/2017
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Matej Košík, 11/04/2017
        Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7, Kenneth Roe, 11/05/2017