[proof] Add proof save path for equations.

We add the and routine the regular proof save path of Equations was
using.

I don't understand what is going on here, these are a few remarks:

- Equations does capture `sigma` at the time of `start_dependent_lemma`
- A custom hook is also captured, along with telescopes
- The shrink function seems like a duplicate with things already in Coq's
  [abstract.ml / declareObl.ml]

I guess the preferred option would be to merge this with the
obligations save path; but I need help from experts.

0 files changed, 0 insertions, 0 deletions