coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Ltac2: equivalent of Ltac1 "eval redexpr in term"
Date: Mon, 24 Jun 2019 15:45:34 +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:mkOq9B2Qt+nmJr9lsmDT+DRfVm0co7zxezQtwd8ZseIeLfad9pjvdHbS+e9qxAeQG9mCsbQd0aGH7uigATVGvc/Y9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMqMUam5ZuJrg+xhbNonZDZuBayX91KV6JkBvw+9q88IR//yhMvv4q6tJNX7j9c6kkV7JTES4oM3oy5M3ltBnDSRWA634BWWgIkRRGHhbI4gjiUpj+riX1uOx92DKHPcLtVrA7RS6i76ZwRxD2jioMKiM0/3vWisx0i6JbvQ6hqhliyIPafI2ZKPxzdb7bcNgHR2ROQ9xRWjRBDI2icoUPE+QPM+VZr4bhqFQDtgGxCRWoCe711jNEmmH60Ksn2OohCwHG2wkgEsoAvHrJq9X6KqgSUfyvzKnP1TXPd+5d1zD86IfUchAuu++DXbZ+fcHMzkQvEgLFgUmQqYP/ITyV0v4Bs3Oc7+V+WuKvl3QnqwZpojW0x8csjJXJiZwRylze6Sp5x4M1KMS+RUVmb9CkF55QuDubN4twWs4iQmdouDokxb0Co5K0YTYFxZI6zBDcc/yKa5WE7xb9WOqLITp1hGhpdbKhixqo7ESs1+3xWtGp3FtLoCdJiNfBu34X2xDN5MWKTuFx8lqi1DqSzwzf9+BJLEQumabFK5MszaQ8moQJvUjeHiL7nEP7h7KMeEo+4Oin8eHnb63mppCCM490jRnzMqEhmsOlHOg1PRICX2md+eSgyrLj+Vf1T6lNjv0ziqXZsZbaKtoHpqOhHgNY1pgv5wy/AjqmytgVnWcLIEhYdB6aj4XlI1TOL+r5Dfe7jVSsijBrx/XeM73kA5XCMnjDn63/crZ58UJc0w0zws5Q55JIELEBJ+rzV1TwtNzeEh82LQi0z/z7B9V604MSQXiPDbOBMKPOrV+I4foiLPWLZI8MoTryN/wl5+P1gnIigl8cfayp3YMNZ3yiH/RmJV+ZYXv2jdsbH2cKpFl2cOu/wlaFSHtYY2u4d6M6/DAyToy8R8+XTYe0xbeFwS2TH5tMZ2kABEraQlnycIDREcwLZS2OOMh51nQhVLOhQoIln1n6sQ7xy7NqKqzP/SAXqYjkzPB04fHekVc58jkiXJfV6H2EU2whxjBAfDQxxq0q+RUgmGfG6rBxhrljLfIW5/5NVV5lZ5vTxrUmTdH0Rg/FONyOTQT+G4T0MXQKVts0huQ2TQN4EtSmgArE2nPzUb4Ti7GPQpcz9/CFhiSjF4NG03/DkZIZoRw+WMIWbD+ngLJy807YAIuby0g=

Dear Coq Team,

I wonder if Ltac2 has an equivalent of Ltac1’s “eval redexpr in term” construct.

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