Open lastland opened 4 years ago
The float_let tactic (defined in https://github.com/antalsz/hs-to-coq/blob/d4b61b81323014fa3b7f127df637dfac9afc408c/examples/ghc/theories/GhcTactics.v#L44-L60) is broken under Coq 8.10.2. I think it's a bug of Coq itself, and I have opened an issue here: https://github.com/coq/coq/issues/11389
float_let
As before the issue gets fixed, I have a temporary workaround that works with our existing proofs: https://github.com/antalsz/hs-to-coq/commit/74e83ea7ffc558ff778678597139dcd87f58b94f#diff-4c03f5269c19d75442f5862b0de92ef1
I'm recording this here, to keep track of the issue, and so that anyone who runs into the problem with this tactic knows what happened.
The
float_lettactic (defined in https://github.com/antalsz/hs-to-coq/blob/d4b61b81323014fa3b7f127df637dfac9afc408c/examples/ghc/theories/GhcTactics.v#L44-L60) is broken under Coq 8.10.2. I think it's a bug of Coq itself, and I have opened an issue here: https://github.com/coq/coq/issues/11389As before the issue gets fixed, I have a temporary workaround that works with our existing proofs: https://github.com/antalsz/hs-to-coq/commit/74e83ea7ffc558ff778678597139dcd87f58b94f#diff-4c03f5269c19d75442f5862b0de92ef1
I'm recording this here, to keep track of the issue, and so that anyone who runs into the problem with this tactic knows what happened.