coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] setoid_rewrite with term vs hypothesis

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] setoid_rewrite with term vs hypothesis
Date: Tue, 11 Jun 2019 17:26:57 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f52.google.com
Ironport-phdr: 9a23:d5zcIh0EtObV4PKGsmDT+DRfVm0co7zxezQtwd8ZseIWKfad9pjvdHbS+e9qxAeQG9mCsrQd1rSd6fCocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSexbalvIBi2rAjdudcajIh/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6JVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOtEtIb9p1oOrQC+BQayB+Pk1yNFhnns0q08zusqDAbL0xY7ENIOsXTUt9X1O7kRUeyv1qbIyy/Mb/VL1jvn6YjIcwwhof6XULJ/dMre00gvFwffglqMrozlOiqY2+IQuGaV6OpgUPigi28hqwxpvjevwd0sio/XiYIRzlDI7zt2z5soJdC+VUV1YsakHYNOuy2GM4Z6WMAvTmFytCony7ALuIS3cSgUxJkh2hXRceaIc5KS7RLmTOuRISl3hHZieL+ngha960mgyunlWsm111ZGszNJktfMu3wTzRDT5c+HSvxy/kelxzmDzRzc6uZBIUwslKrbLYAuwqIom5YNrUjOGjX6lUb2gaOMa0kp++ml5/7nb7n4vpOcMpV7igD6MqQggMy/BuE4PxAUUGeA+eS81abj/U3nT7VJlPE5iK/Zv4rcJcsGvKK5Ag5V0pos6xukADem1c4XnXgDLF5fZB2HiI3pN0nUIP/kFfe/n0iskDBzyv/aOb3hG4zBIWTHkLf8Zrlw8FVcyQo2zdBH/Z1YELABIPTpWk/wrtPUFBE5Mxbni9rgXd56z8YVXX+FSvuSN7qXuluV7MouJfONbckbomCuBeIi4qvHh384gl8QfuGA25IRZDjsF/5mIl6ZbHmqi9EIF2tMvwsiQ8TljVSDVXhYYHPkDPF03S0yFI/zVdSLfYuqmrHUhH7qTK0TXXhPDxW3KVmtcoyFX/kWbyfLe51ulzUFUf6qTIpzjEjz5j+/8KJuK6/vwgNdtZ/n04IotejalBV39DstSsrAiSeCSGZ7mm5OTDgzjvgm/R5Nj2yb2K09uMR2UMRJ7qoQAAg/PJ/Yied9DoKqVw==

For a term t, the following fails with error "Ltac call to "setoid_rewrite (orient) (glob_constr_with_bindings)" failed. Tactic failure: setoid rewrite failed: Nothing to rewrite.":

setoid_rewrite t

But the following succeeds:

pose proof t as Hx.
setoid_rewrite Hx.

This is surprising to me. Is this necessarily a bug?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] setoid_rewrite with term vs hypothesis, Abhishek Anand, 06/12/2019