coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ltac2 retraction bug?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Tej Chajed <tchajed AT mit.edu>
Cc: coq-club AT inria.fr
Subject: [Coq-Club] Ltac2 retraction bug?
Date: Wed, 22 Apr 2020 16:36:41 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f177.google.com
Ironport-phdr: 9a23:bqxfwhWIZF+XeQWQ59Ln3/NHRujV8LGtZVwlr6E/grcLSJyIuqrYbRSEt8tkgFKBZ4jH8fUM07OQ7/m9HzBfqs/a7TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrQjdrMYbjIltJqosxBbEomZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zMlMd+kLxUrw6gpxxnwo7bfoeVNOZlfqjAed8WXHdNUtpNWyBEBI63cokBAPcbPetAoYfzp0UAowa9CwauCuPhzTBHiWP506Ahz+QsExvL0BA6Et4SrnjZqsj+OqcIUeCyyanF1TvPb/FR2Tf76YjIcQ4uofWSUr1uasfRxkwvGBnEjlWUs4DqIzSV1uEDv2OG6OdgV+Wvi2gmqwFyvDevwtkjhZfSi4Iaz1DL7yR5wIIvKdKkT057ZMepHZ1NvC+UMIt2R9ktQ2BuuCsixb0GuIK7fCgXyJs83RLQd/uHc42O7xn+V+iROS91iGx5dL+7nRq/8kitxvfhWsS1zFpGtDdJn9vOu3wVyRDe69SLRuZ480u83TuAywXe5+5FLEwoiabWLoMuz74qmZcWrEvOHTT5l1vzgaKZbUok9Oao5uHpYrr4p5KTKYp5hwXiPagwh8OyB/kzPBIUUGiB4+u80aXu/U3nT7VOif07iqzZv4rbJcQfv6K5GhNV3ps65xaxEjur0tYVkWMILFJCfxKHgIzpNE/ULP/kCve/hkygkDZtx//YIr3sGovBImTHnbv7frtw61RQxBcywNxD/Z5YF7MMLfDrVk/0rtPYDxs5MwKuw+bgDdVwzoEeWWWJAq+YM6Pdr1uI6fwxLOSXa48VvSzyK/kh5/L0kXA5nlodcbGz3ZQLcHC4AuhmI0KBbHXwhdcBCH4GsRY6TOz3k1KPSiVTZna3X6Ik/D43EoOmDYHZRoCsmrONxim7HocFLlxBX2yBEz/Dd4yGVvtEPD6ZIsZjnzAsULm9DYItyEf9mhX9zu8tLO3S+y4VsZ/u/Ndw7uzX0xo18HY8W8aa1WCOQmV5k0sHQjY32OZ0pkkrmQTL6rRxn/ENTY8b3PhOSApvcMeEl7UrWeC3YRrIe5KycHjjR9ynBT8rSddomo0BZk98H5OpiRWRhnP3UY9QrKSCAdkPyoyZ33X1IJwjmXPP1a1klkV/B8UWajLgial4+AzeQYXOlhfBzvr4ReEnxCfIsVy74y+WpkgBCVx/VKzEWTYUYU6E9dk=

On Wed, 22 Apr 2020 09:23:01 -0500
Tej Chajed
<tchajed AT mit.edu>
wrote:

> I've written an Ltac2 tutorial
> <https://github.com/tchajed/ltac2-tutorial> with a handful of
> examples and detailed explanations.

I've been trying out Tej's ltac2_tutorial.v, and think it uncovers a bug
in retraction of some Ltac2 globals, unless my environment is
somehow triggering the problem. All I did was: in ProofGeneral, click
Use to process the whole buffer (which works), then click Retract,
then click Use again. The second Use dies at the "++" Ltac2 Notation
with the error:

Error: Syntax error: [input_fun] pr ':=' expected (in [tac2def_body]).

I'm using Coq 8.11.0. Could someone verify that this isn't only me
doing something stupid?

[Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Jason Gross, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Tej Chajed, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
  - [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] Ltac2 retraction bug?, Maximilian Wuttke, 04/22/2020
      - Re: [Coq-Club] Ltac2 retraction bug?, Pierre Courtieu, 04/23/2020
        
        Re: [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/23/2020