Pierre-Marie Pédrot
Pierre-Marie Pédrot
The whole tactic engine has been rebuilt precisely around the fact that the notion of child goal does not make sense in general. By contrast, the pre-8.5 engine was based...
> Does this really matter, though? In practice, aren't most tactics are still more or less goal → list goal, even if the engine itself is list goal → list...
> Does the following capture the issue you have in mind? Indeed. > In that case it looks like that the parent of the evar that gets created by apply...
@coq/doc-maintainers Can some maintainer assign and merge? This seems ready and is needed for the 8.16 release.
@herbelin this is still waiting for an overlay for Equations.
This doesn't seem ready, removing the milestone. It's a minor change and should be easy to fix though, @herbelin if you do it before the branch it can still go...
Still present as of dc01d6d69d5af9f4c95962ae8ed47151fbe8fd1b.
Apart from the `tc_transparency_locality` one (which does not matter because it's not deprecated in #16004 yet), these are superglobal entries that cannot be tweaked through attributes. They were thus not...
That's an interesting observation for backwards compatibility, in any case.
@JasonGross this option only applies to auto hints indeed, not rewrite hints. It's a hack anyways, I don't think it's really reasonable to implement the same thing for rewrite hints...