coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term"

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term"
Date: Tue, 25 Jun 2019 08:36:22 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.600.7
Ironport-phdr: 9a23:1G3Tvh3Pu3cQ/DexsmDT+DRfVm0co7zxezQtwd8ZseIfK/ad9pjvdHbS+e9qxAeQG9mCsbQd16GO6OigATVGvc/Y9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMqMUam5ZuJ6k+xhfVrHZDZuBayX91KV6JkBvw+9q88IR//yhMvv4q6tJNX7j9c6kkV7JTES4oM3oy5M3ltBnDSRWA634BWWgIkRRGHhbI4gjiUpj+riX1uOx92DKHPcLtVrA7RS6i76ZwRxD2jioMKiM0/3vWisx0i6JbvQ6hqhliyIPafI2ZKPxzdb7bcNgHR2ROQ9xRWjRBDI2icoUPE+QPM+VWr4b/plsBsRSxCBK2C+/zzjJFnGP60bE43uknDArI3BYgH9ULsHnMotn7KaASXv66zKnU1zXDaOtW1S/g44bPcxAuvfGMUqhufsrVx0UkCgTIjlCRqYP5PzOazPoCs2yB4+p7UuKglWEnqx1rojio3schkYjJhoQJyl/a8SV12po6Jdq9SENiZ9OvDZVetyafN4RsQ8MiRXlluCc8yr0ap5G7eDIGx4k5yBPZdveJcJCI7wr+WOuVPzt0nnJodbKlixuy70Ss0PDwWtS03VpSsyZIk9fBumoD2hHd8MSLVPVw80O71TqS1A3f9vlILV01mKffMZIt3L49m5UJvUjdBCP6hUX7gauQe0454Oan8f7nba/jppKEN497lAX+MqM2l8y6DuQ3KBUCUmeB9eS90r3j4VP2QLFQgvIqlanZtYjWJcUdpqGnHw9Yypsv5hKhAzu80NkVnWMLIVJbdB6dkoTlJlHDLOj9DfilglSslDlrx+rBPr3kGpjNK3nDn6vhfbln9UFczBA/zctY551KBbEBPOjzWkjptNHDDx85NRC0zPjjCNlnyoweXmePDreDMKzOqV+I+v4vI+6UaYAJvzb9MuEp6OLqjX8kglAQZrKp3JsSaHCgBPtqOUSZYXz2gtcAC2gGpAQ+TPa5wGGFBHRYYG/3VKYh7Bk6DpinBMHNXMrl1LeGxWKwGoBcTmFAEFGFV3nyIdaqQfAJPWipJcJujiYDTfzpbo4q1RijsEWyn79mJerd9ylerpXu28Rv4PX7lBcu+DgyBMOYhTLeB1pol38FEmdllJt0plZwnw/ajPpIxsdAHNkW3MtnFwc3MZmFkL5/BNmrBkTAeMuETBCtRdD0WWhtHOJ0+McHZgNGI/vnlgrKhnP4ArkJmrjND5sxoPqFjirBYv1lwnOD75EPylwvQ89BL2qj3/ct9g7PCoqPmEKcxf+n

Dear Jason,

thanks for the pointer! I will grep through the Ltac2 files for “external” and make some documented list of this.

I don’t fully understand your comment on Declare Reduction. To me this looks identical to what can be defined in Ltac2’s Std.red_flags type.

I will look into making some Ltac1 compatible wrapper notation, as you suggested.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Soegtrop, Michael, 06/24/2019
- Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Jason Gross, 06/24/2019
  - Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Jason Gross, 06/24/2019
  - RE: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Soegtrop, Michael, 06/25/2019
    - Re: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term", Jason Gross, 06/25/2019