Somehow fixing a side-effect bug in tactics-in-terms.

Before this patch, when tactics-in-terms were relying on the ugly environment-
modifying primitives such as tclABSTRACT, the returned term was ill-typed
because the resulting effects were just dropped. Now we modify the returned
term on the fly, effectively getting rid of the effects it may depend on.

Yet, this is not completely satisfactory, because the tactic may solve some
goals at distance (I would have said by side-effect, but this is ambiguous
here). If ever the resulting terms are depending on the side-effects of the
tactic, then we are still unsound.

This patch should handle most of the use-cases gracefully. To really solve this
issue, we should rewrite the pretyper in the new monad, which is easier said
than done.

0 files changed, 0 insertions, 0 deletions