coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to rewrite, needed to match goal

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to rewrite, needed to match goal
Date: Wed, 30 Dec 2020 00:38:20 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f181.google.com
Ironport-phdr: 9a23:gqdlyB9jBvAMP/9uRHKM819IXTAuvvDOBiVQ1KB31u8cTK2v8tzYMVDF4r011RmVBNqdsagewLqM+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhKiTanf79+Mgu6oQrSu8UInIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahNFugqJVoByvpBJxzIDbb46XKPVwcbjQfc8YSGdbQspdSyJMD4G6YoASD+QBJ+FYr4zlqlYQqRu5HwysC/3pyj9UnnD4x6w60/g4HQzY2AwvBc8Ov2nKo9XxKawfVvy6zLHJzTXfc/xW3S3y6JXVfR8/pfGBRr1wcc/LxkkuEwPJlEmfqYvgPz6M0OkGrmeU4fZ6W+21l24ntx9+oiKpxso0loXEgowbxF7Z+Sh4z4s4JsG1RVJ0bNO4EJZdtC6UOpZ2TM4jR2xkpSY3x6MatJO0fCUHypAqygDcZvKIcoWF5hTuX/uSLzdgnH9pZq6zihKo/UWjyuDwTNS43VdWoiZfj9XBtW0B2wTN5sWIUPdw/1qt1SyR2w3c9u1IO0M5mbbdJpU82LA/jIATvl7GHiLumEX5kquWdkI89+it8evnY7HmqoaFN49olw3yK6oultG8DOglKAQOUG+b+eOz1L3n40L1WqlFjvozkqXBsZDaI9oUprKhDgNLzoou7wyzAjSm3dgCgHUKLU5JdAiag4XqJl3COPX4Au2+g1Sonjdr3ffGPrj5D5rRNnjDkavhcqp560FG1Qo80M5Q55ZPB7EOJfL8QE7xtNjCAhAlNAy0xv7rCM9h2YMGRWKPHqiZPbvOvl+P/+IjOvWDZIsIuDnmMPUl/P7vjXohmVAHZ6Wp3J0XaGq5Hvt8OUmZb2Ds0Z89FjIBuRN7R+j3gnWDVyRSbjC8RfES/DY+XamijILOQJyauL2dmQy/F4Baa2QOXluUEGvjc4yZV/oIQC2XK85l1DcDUO7yGMcayRiyuVqimPJcJe3O93hA7MOx5J1O/+TW0CoK23lxBsWZ3XuKSjgtzGwNTj4ymqt4pB4kkwrR4e1Dm/VdUOdrybZJXwM9b8COyuV7D5XrRluEcI7ZERCpRdKpBTx3RdU0kYdXPxRNXu66hxWG5BKERqcPnuXSVpMx+6PYmXP2IpQlxg==

On 12/29/20 11:55 PM, Jeremy Dawson wrote:
> Hi Clement,
>
> Thanks - but this doesn't help.
>
> Ie
> Set Printing All.
> Show.
> then Check (cut and paste from the goal, with lots of @ everywhere)
> still gives the error,

Hm, then I'd need a concrete example to say what causes the issue.

[Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
  - Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/17/2020
    - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
    - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/28/2020
      - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
      - Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020