The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> 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 can write

  Declare Reduction foo := cbv beta delta [bar baz].

and then I can `eval foo in qux` in Ltac1.  I believe in Ltac2, I need to redefine the reduction strategy to make use of it, and cannot use the name given by Declare Reduction.

On Tue, Jun 25, 2019, 01:36 Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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