[program] extend obligation to give back a mapping from obligations to

terms

This is necessary for programs like Equations that call add_definition
and want to later update in their hook some separate datastructures
which refer to the obligations that are defined by Program. We give back
a map from obligation name to a constr defined in the program's universe
state which the hook returns as well. (Obligation names also correspond
to undefined evars in the original terms through
Obligations.eterm_obligations).

Using this, I can avoid ucontext_of_aucontext in Equations, allowing PR
 #8601 to go through.

0 files changed, 0 insertions, 0 deletions