coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about writing plugins/vercular commands extension

From: Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about writing plugins/vercular commands extension
Date: Fri, 31 Jan 2020 13:07:50 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=zoe.paraskevopoulou AT gmail.com; spf=Pass smtp.mailfrom=zoe.paraskevopoulou AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f174.google.com
Ironport-phdr: 9a23:bYIdDxJscAo6T0cp2NmcpTZWNBhigK39O0sv0rFitYgeLvvxwZ3uMQTl6Ol3ixeRBMOHsq4C17Kd6vi4ESxYuNDd6StEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQZjId4Jas91hTFrmZUd+hK2GhkIU6fkwvm6sq/4ZJu/T5ct+49+8JFTK73Y7k2QbtEATo8Lms7/tfrtR7NTQuO4nsTTGAbmQdWDgbG8R/3QI7/vjP1ueRh1iaaO9b2Ta0vVjS586hrUh7ohzwZODM/7Wral9Z/jKNfoBKmuhx/34vZa5ybOfZiYq/Qe84RSGxcVchTSiNBGJuxYYsTAOUOIOhWoYf9qUUMohW9AgehH/ngxiNNhnLs3a02z+YsHAfb1wIgBdIOt3HUoc32O6cVT+++0bPGwi/Zb/xMwjf965bHcg4mofGUWrJwbM7RyU4yFwjYiViRqIvlMC2P2uQVqWeb9fBvVfmsi2E5tQFxpSCvxsAxionNgYIV10vJ9Sp8wIkvJN24TFR3bsKjEJtVriyXMZZ9TMA6Q2xwpio21rkLtYS4cSUK0pgr2h/SZ+Cdf4SV4B/uW/6dLSp3iX55Yr6zmhW//VS6xuHiWcS4zExGojRLn9TDsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU00kLDUK58lwrIpj5oTrVnPEjb4mEnrjqKbeV8o+uev6+TgbbXmooGTO5VohQH5N6Qigs2/AeImPQgSR2WX5/iw2bn58UD6QLhGlOA6n6jFvJzAOMgWpKG0DxdQ0ok56ha/Czmm0M4fnXkCNF9EeRWHgJbzN1HWOv/4F+2wg0+vkDh12fDGOaXhApLQLnjHl7fhYK1w60FZyAUpzNBf44hYBa0GIPL2QkPxrsDXDgclMwyoxObqEMly1oQHWW6WHqCZNL7SvkST6+I0I+iMYZcVtyznJ/gk4f7ul345lkUHcamnx5tEIEy/S/9hOgCSZWfmqtYHC2YD+AQkH8Lwj1jXYzleL067Rasn5TwlD5qhEIPEW8j5kruMmj+yBJRNZW1YDUiLDHPvaq2LXv4NbGSZJco3wW9MbqSoV4J0jULmjwT90bcydrOJqB1djorq0Z1O38OWlRw28mYqXcGU0mXIVn0t221RGGNw06d4rkhwjFyE1Pog2q0KJZlo//pMFzwCG9vZxu1+Bcr1X1uYLNiMQVeiBN6hBGNoF45j85o1e094Xu6aoFXbxSPzWu0akrWKANo/9aeOh3U=

On Jan 31, 2020, at 12:55 PM, Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com> wrote:

Ah, that’s an interesting observation. My file is an .ml4 file (which seems deprecated for this purpose, but I never knew until now) and the syntax is exactly the syntax that I use in the file (in fact the {} syntax gives me a syntax error in .ml4). But I’ll try to change it to .mlg and see if that works.

My file is an .ml4 file (which seems deprecated for this purpose, but I never knew until now) and the syntax is exactly the syntax that I use in the file (in fact the {} syntax gives me a syntax error in .ml4).

Actually, it seems that for the version of Coq that we’re using (8.9.1) there’s support for .ml4 files only.

[Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/30/2020
- Re: [Coq-Club] Question about writing plugins/vercular commands extension, Talia Ringer, 01/31/2020
- Re: [Coq-Club] Question about writing plugins/vercular commands extension, Gaëtan Gilbert, 01/31/2020
  - Re: [Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/31/2020
    - Re: [Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/31/2020
      - Re: [Coq-Club] Question about writing plugins/vercular commands extension, Talia Ringer, 01/31/2020
        
        Re: [Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/31/2020