coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <aa755 AT pm.me>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] why are hints inside sections forbidden?
- Date: Fri, 20 Jan 2023 12:40:48 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=aa755 AT pm.me; spf=Pass smtp.mailfrom=aa755 AT pm.me; spf=Pass smtp.helo=postmaster AT mail-40133.protonmail.ch
- Feedback-id: 39498114:user:proton
- Ironport-data: A9a23:wnGelq432uKn4S64LqxJbAxRtC/DchMFZxGqfqrLsTDasY5as4F+v mZJWGGBa/reYWChf41ybty2o0xT75DWy9EySAM4qioyZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UYYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhnglbQr414rZ8Ek05K2o4GtC1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6/IpUHhvOaczwMotAlER+ 9YKdTQMSynW0opawJrjIgVtrsEqLc2uYNtG4Som1SveEfEgRJnCR+PB5be03h9p1p0IQq6YO 5JfMGE0BPjDS0Un1lM/AZthwbqAnny5djAwRFe99fppvjmKk1IZPL7FDPmOK4eRfedsg3nB/ 0H/ojjcPjgZDYnKodaC2inw1rSRzHKTtJgpPLa/77thhECZ7ncCDQUfE1q9u/iwzECkM++zM GQR8ysq6PRqrRfwCMHnWAG/pnuNvxpaUNo4//AGBB+lze2I2l+dLEM+YmRCWIMont1rQT0P7 wrc9z/2PgBHvLqQQHOb076bqzKuJCQYRVPugwdaFGPpBPG9+ukOYgLzosVLTPHs0oGkcd3k6 2DT8XVm71kGpZdTj82GEUb7byWEjbihc+LYzgDeX2bgslsgP9Xjf5av9V/d6P9BKMCSTjFtX UToeeDAvIji7rnXzkRhpdnh+pn1uJ5p1xWA3jZS82EJrWjFxpJaVdk4DMtCDEloKN0YXjTif VXevwhcjLcKYiT2NPIsO9jgUplwpUQFKTgDfq6NBjapSsYqHDJrAAk3DaJt9zq2yBREfV8XY MzHGSpTMZrqIf87nGHoFrZ1PU4D3jo52WTVDZn0pylLIpLADEN5vYwtaQPUBshgtP3siFyMo 753apXWoz0CDryWSneMq+Y7cwtVRUXX8Lit9qS7gMbYflE5cIzgYteNqY4cl3tNxfUMx7eYo ivkMqKaoXKm7UD6xcyxQigLQNvSsVxX9BrX5AR8Ygr66Gtpeou18qYUer0+eLRtpqQpzud5Q 7NBM4+MC+hGAGaPsTkMT4jPnKo7fjSShCWKI3WEZho7dMVeXADnwILvUTbu0ygsNRCJk/UCj Yeu7S7lZKYSZh9DCZ/WYc2/zlnqsnk6nvlzbnTyIdJSWRvN9dFqIhPuktkbCtEpOzDezRu4y Qq5UAoSmsfVqaRo8tDipLulqr2xGLBUBXtqHGj87Je3OxLF/2Gl/5RybeaQcR3ZV0L24K+Hd 8wM693dadosgw9sn6RwN51J3JAOzYLjiJECxzs1AUiRSUqgD41RB0Wv3O5Nh/Vr/aBYsw7nY XC/0IBWFpvRMfy0DWNLAhQua9mC8vQmmjPyy/ARC2ei7Q9V+Iu3a2ljDyOuugd8coQsaJgEx N0/svE48wa80xomEuiXhxBuqlijECYybLUFhLo7Xqnb0hEm23NTU6z6UyXW2qyCW/9IE0stI wKXupb8uqRh9hLCXkc3RFfw3rt7pJURuRp14kcICHaXl/Hk2PIm/h1j3g4mbwZSzx5oi/95B VVqE2ZXJqy+2Shiq+YefmKrGiBHXAa4/G6owXQ3tWTpdWuafU2TE38cYMGjpFs49UBYdRhlp ICo8n7vC2vWTZugzxkMVl5AgN29a95Irynput2tRuaBFLkEOQvVuLekPzc0mkG2EPEKpRP1o Mdx97xNcoz9DykbppM7B6S81bg9TBOlJnRIccp+/ZEmTH3tRzWv5Qegc0yBWNtBB/jvw3+KD 8ZDIsFuVRPn2h2e8REdJ6oHeIFvkNATudEtR7LMJEw9iYW5kAZHipzqy3XBtDcZeOk2yccZA aHNRg2GCV2V1Cd1mXeSjcxqOViYQNgjZS/j1tvo7NcyNokitdt0ehoYyYqEvHSyMSpm8SmLv QjFWbTk8ux6xalonKruCq9mBTjoGejsVe+Nzh+/g+5OYfzLL83KkQEf8XvjACh7IpoTXI5Ru YmWkduqwn7Agqk6Y1rZl7aFCaNNw8e4B8hTE8DvKUhljTmwY9Dt7zQD6lKHB8Rwyv0F3faeR iy8dMeUXvwWUY0ExHRqNg5vIyxEAKHzNqrdtSexqsqXMSck0CvFEoKXxSe8JyUTPCoFIIb3B QLIqu6jrIIQ5phFABgfQepqGdlkKVvkQrErbMD1qSLeNGSzn1eeofH3oHLMM90Q5qWsS64WI K4pRyQSsDy3saDMiY0B6tcp+AUNC2p6h+w5f0Zb8N4eZ/WSEjsdNepEWXkZIsg8r8Aw/MiQi PLxgK8KESC7WDksndDU/oH4RgnGbgAREo6RG9Hqln94rw+uAcWFDdONM8umD2heIlPe8Q1sF T3SFrAc8PR8LlGFiNv/PsCGvNo=
- Ironport-hdrordr: A9a23:L4o30azeMA80BlLXQaAPKrPwNb1zdoMgy1knxilNoH1uA6+lfq WV9sjzuiWetN9vYhAdcLy7VJVoIkm9yXcW2+cs1N6ZNWHbUQCTQ72Kg7GO/wHd
- Ironport-phdr: A9a23:WZ2M6hAws48lzRPe2nfqUyQUdEgY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8wygaQB86HsLptsKn/jePJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNYwhEniexba5sI Bm5ogjcuNQdjJd/JKo21hbGrXxEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2V KRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+4 6t3ThLjlSEKPCM7/m7KkMx9lKxVrgyhqRJiwIDbb52aOeFkca/BZ94XX3ZNUtpTWiFHH4iyb 5EPD+0EPetAs4TyvFsOrRqlBQmsGuzvySJDi2Pw3aIg1eQuDBzN0Qs6EN0UsnnZrNX4ObwKU eCw1qXIyCvMYupQ1Dzg54fGbgovruuQXbJsb8XR008vGhvZglieqIHrMDeY2+cNvWWF7eduV e2hhmEnpg1svDWhxsMhh4vJiI8UyV3I6CZ0zYk6K9O2VEN2ZcOpHZpOuyyGMYZ9X8AsQ3lwt SonybALuYS3cSoWxJg9yBPTd+aLf5WG7x/tUuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtKq zBKktjItnwU2BHf9tWLR/Vz80u7wTaPzQfT6v1DIUAykKrUMZ8hwroqmpUPsUTPBi72mEPog 6+Kbkgo5+ul5uT9brjkupOQLYB5hh3kPqgzlMGyD/w0Mg0UUGia/eS82qfj/Ur8QLhSlPI5i KvUvZDaKMkAvq65BhVZ0oM95BqnCTepy8wXnWMbI1JdZBKHk4/pNknTLPzgF/ewn0yskCt3x /DBJrDuHpLNLmHanLj9ebZ99lVTxREozdFf4pJUEqsOLOjyWk/3rtzYDwU2Pxa6w+b9W51B0 dYVXnvKCauEOuuGuliRo+krPuOkZYkPuT+7JeJztND0inpssFUdfLKp0JhfQXaxGPgud0yQP iexqs8EV2IH6FltBNf2gUGPBGYAL025WLgxs2lT4OOOCI7CQtrom7mdxGKhGZYQYGlaC1eKG HOudoOeWv5KZjjBatR5nGkiUr6sA5QkyQnorBXznrNucbeJ0jUd85fuh5Bu/+OGrRgp7nRvC tiFlWSETmV6hGQNEjY/g/0iiVR4jFKOguBjm/INLdVI/LtSVxsic57Ry+svE9fpRgfIZcuEU n6jS9SiRG1pF4lqhccUZFp6HdCrjxSF1CrC76Y9sbuNCdR096vd2yK0PMNh0zPc06JniVA6Q 8xJPGngh6hl9gGVCZSb20Oe372nc6gRxkuvvC+K0HaOsUdEUQVxTbSNXHYRYVHTpMj44UWKR qGnCLAuOA9MgcCYLa4CZtrshFRADPDtXbaWK2u4xDrtLQ6NgLaBLcLrd2gbwCTBGR0ciQlAt X2CNAU4GmKguzeHXGEoSgqpPxuqqLIl+xbZBgcuwgqHblNsze+w8x8R37mHTu8Lm6gDs2Eno il1G1C025TXDcCBrkxvZvY5A5t17VFZ2GberwE4MIanKvUoj1dBLllfp0ao0hg9Wc1Q1NMnq n8n1l84IKvHjQ5pbzbe2J26adi1YiHiuRuobaDRwFTX1t2br7wO5PoPoFLmpAi1F0Am/h2Ly vFt2mCHrtXPBQsWC9fqV1ovsgJ9rPfcazU84IXd0TttN7O1u3nMwYBhCOwgwxemN9BRVcHMX Ab7TJBHL9Crbukn01SkdRMLOulO+bV8ZpP7MaTenvLzer87x3qvlixf7Zp4016Q+iY0UePO0 5sfgpT6lkOGWzr6kFa9o5XykIFAaysVGzn3wizlCYhNI6xqKN9bVCHxe4vrnpMn3MW+PhwQv ESuDF4HxsKzLB+bblinmBZVyVxSu3us3y2x0z1zlTgt6KuZxi3Hher4J39lciZGQndviVD0L M26ldcfCQKhZld0yTO94AD/yuII7LQ6NGTVTUpSKmL/Jj4/D4Oos/yHboQcjfFg+TUSW+O6b 1eAT7f7qBZPyCLvEVxVwzUjfi2rsJH0zFRqzXiQJ3FpoD/FaNl9kF3BscfES6cbjV9kDGFoz CPaDV+mM5y18MWIwt3d5/umWTvpV4UPI3C7kMXf7G3nvSsyRkfj1/Grxo++QVV8jne9i4AsD WKS8HOeKsHqz/joaLI6OBYwQgOnrZI9QN02k407gIwc1CotnY2bpzwfi2DvNtNe0KP6KnEND SgCx9qfiOT88HVqNWnBh4fwV3HHh9Bke8H/eGQdnCQ088FNDq6Qqr1Chyp85FSi/0rdZv10n zFVzvVLijZSm+YSpA8k1TmQGJgXFEhceHC0zk/Tqcikq7lQYmOmcLz230o2kd26Db6Eqx1RQ z6gKspkQnc2sp05aQmXtR+7ooj/MMHdd9cSqgGZn1/bgu5ZJYhw3vsGiCx7OH7s6H0oz+lox Rdq3Jy8oM2GMzA0rP//XUYeamWzPphIqVSPxe5Ek82b3p6iBMBkEzQPBt7zSO6wVSgVvrLhP hqPFzs1rjGaH6DeFEmR8hQDzTqHHpa1OnWQPHRcw89lQUzXLUUA3V08RDB8m5NzRWXIjITxN Vx04Dwc/AuyshxX1udhLAXySE/arQasL2tsEcPEagJM6R1F4ULcMMjY5eI5TEQ6ttWx6QeKL GKcfQFBC2oED1eFC17UNb6r/dDc8uKcC7n2P77UbL6Js+AbS+aQyMflzN595zjVfJbqXDEqH 7gh10FER3w8B8nJh2BFVXkMjyyUJ8+D+EXlqnAx8Zj5rKytAVm0rZ2GD78YWT2K0wizx6KOZ bb4bMdRLD9Z0tZQnSaTk/4HxlkOjCdrfjipV78A53elpE34gqoRChNJMktO
- Ironport-sdr: 63ca8bdc_f2fSlLDioabMpzp4kt0GDK1lSDFTGXN9TwXoe2jo49g6uxy GG87I+P/nMui5DWhfjdVPzJilFJysGBL05m0PKA==
Are there some technical difficulties in having `End Section` re-add the `Resolve`/`Rewrite`/.. hints (maybe only those declared with #[global]) declared in sections after generalizing the terms over section variables?
--
Abhishek Anand
- [Coq-Club] why are hints inside sections forbidden?, Abhishek Anand, 01/20/2023
Archive powered by MHonArc 2.6.19+.