coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] question about ltac semantics

From: Andrew Harris <andrew.unit AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] question about ltac semantics
Date: Wed, 1 Feb 2017 09:50:31 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andrew.unit AT gmail.com; spf=Pass smtp.mailfrom=andrew.unit AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f43.google.com
Ironport-phdr: 9a23:qjNqXxFtoZKW2pf0ABCQB51GYnF86YWxBRYc798ds5kLTJ76oMiwAkXT6L1XgUPTWs2DsrQf2raQ7f+rADRYqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t1b/rM4T1KJkJrw81VPpq2FSev8ekWpuKUiegFDh4Mas1JFm+iVU/fkm8pgTAu3BY60kQOkAX3wdOGcv6ZizuA==

Hi,

Ltac t :=
    repeat (match goal with
              | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
                dep_destruct E
            end; crush).

[Coq-Club] question about ltac semantics, Andrew Harris, 02/01/2017
- Re: [Coq-Club] question about ltac semantics, Andrew Harris, 02/01/2017
  - Re: [Coq-Club] question about ltac semantics, Guillaume Melquiond, 02/02/2017