Stream: Coq users

Topic: `old_hints` in `rewrite_strat`

view this post on Zulip William Mansky (Mar 04 2024 at 18:05):

Can anyone tell me what the difference is between hints and old_hints in rewrite_strat? The manual just says "to be documented". I've stumbled across an example where rewrite_strat fails with hints but succeeds with old_hints (and autorewrite also succeeds).

Last updated: Oct 13 2024 at 01:02 UTC