Coq: rework generation of dependent pairs so that they are only

constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.

Also
- Don't simplify nexps before printing (note that we usually end up
  needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
  because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
  fill in metavariables (because manipulating the goal can interfere with
  instantiating them)
- Update RISC-V patch

0 files changed, 0 insertions, 0 deletions