coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cutrewrite

From: Fabian Kunze <fabian.kunze AT cs.uni-saarland.de>
To: Chris Dams <coq-club AT inria.fr>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] cutrewrite
Date: Mon, 20 Jul 2020 12:00:19 +0000 (UTC)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fabian.kunze AT cs.uni-saarland.de; spf=Pass smtp.mailfrom=fabian.kunze AT cs.uni-saarland.de; spf=None smtp.helo=postmaster AT theia.rz.uni-saarland.de
Ironport-phdr: 9a23:MnB6RRVSl2aZuElZa0he+utINorV8LGtZVwlr6E/grcLSJyIuqrYbBODt8tkgFKBZ4jH8fUM07OQ7/m+HzBcqs/Y+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi3oAnLucQbjoRuJrssxhDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuByvqRxhzYDXYo6VOudwcazBct4BX2VNQtxcWDddDo+gbYYCCfcKM+ZCr4n6olsDtRuwChO3C+Pu0DBIgGL906gn0+QnEADJwhErEtUAsHvOt9r1Nb0dUeavwKnL0DXDafJX1inm5YfUaRAtu+yMXbRxccbI0kkgDRnKjk+UqYP/OTOay/4BvHWF4Od5U++klmEopR1rrDe12scslpfGhpgTyl3c9Sh0zoY4K928RUN7fdOqHpVduSGVOoV5XM8vX3xltSk5x7AbuJO2YCkHxpQ5yhLCdfCLb5WE7BL9WeuTPTt1mHRoc6+8iRaq6UWs1+PxW8au3FtOrydJiNvBumoD2hDO8sSKRfpw8l281TqS2A3f8O9JLVo2mKfdNpUv2KQ/loAJvkTGBiL2mFv5jKuRdkg85uio6/roYrT8qZOGLY91ixvyMrkomsy+GOg4KRIBUHKB+eS4zrLj+1D2TK9XgfIoiqXZsZbaKtoHpqOhHgNY3Iku5wy7AjqnytgVn2MLIVxYdB6fiojmIVDOIPT2DfelhFSslS9mx/7cMbL6A5XCNH7DnK3ifbZg7U5dyRQ8wMtD6JJPEL0BPfTzWk7ouNzDFBA2KRa0w+L9B9V7y4wSQ3+ADbGBPKPIrVCI/v4vI/WLZIINpDn9LOEl6+fygn89hF8SZrKk3YAXaXC9BvRpOV+VYXvqgtcbEGcFpBAyTOLwiA7KbTkGTHaoXrl0yjg+E8ryBoDaA4upnbap3SGhH5QQaHoQWX6WFnK9WYyOWv4KIAGPJN1s2mgKXLKgQoln1gyopgLSwKEhM+zVvzYRvIjn3d55oeHew0JhvQdoBtiQhjneB1p/mXkFEmdvjfJP5Hdlw1LG6pBWxvlRFNhd/fRMCF9oPoWa0up7Tsv7UxjFd9GFDlqrEIz/XGMBC+kpytpLWH5TXtWviheZgXi2A7IUnvqRFtop9KOZxHH4PcJ0zXqA2KRz1wB6EPsKDnWvg+tEzyaWH5TAyR3LnL3saKIdmTXE/X2HxGyC+k1VAlZ9

Hi,

one can do this:

unshelve erewrite ( _ : a=b) in H.

Best,
Fabian

18 Jul 2020 10:11:41 Chris Dams <chris.dams.nl AT gmail.com>:

Dear all,

Coqide says that cutrewrite is deprecated. The docs say that I should use the enough tactic instead. So I can do 'enough (a = b) as ->' instead of 'cutrewrite (a = b)'. This works but what do I do when I would want to do 'cutrewrite (a = b) in H'. I.e., use cutrewrite to rewrite something in a hypothesis?

Regards,

Chris

[Coq-Club] cutrewrite, Chris Dams, 07/18/2020
- Re: [Coq-Club] cutrewrite, Laurent Thery, 07/18/2020
  - Re: [Coq-Club] cutrewrite, Chris Dams, 07/20/2020
    - Re: [Coq-Club] cutrewrite, Théo Zimmermann, 07/20/2020
- Re: [Coq-Club] cutrewrite, Fabian Kunze, 07/20/2020