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: Jun 13 2024 at 21:01 UTC