Karl Palmskog (Aug 07 2023 at 14:05): Karl Palmskog (Aug 07 2023 at 14:05):What is the recommended incantation for using the SSReflect rewrite tactic and as little as possible of anything else from SSReflect? In the refman, I find this:
From Coq Require ssreflect.
Import ssreflect.SsrSyntax.
but is using "just this" recommended/viable?
Context: it was discussed at the Coq Workshop last week that people having unintuitive unification issues may want to just use the ssr rewrite as a drop-in replacement for regular rewrite.
Karl Palmskog (Aug 08 2023 at 11:56):@Enrico Tassi any chance for an "official" recommendation here?
Enrico Tassi (Aug 08 2023 at 11:59):I have not tested it in a while, but if it still works, that would be it.
Karl Palmskog (Aug 08 2023 at 12:00):thanks, I'll try to test then
Last updated: Oct 13 2024 at 01:02 UTC