diff options
| author | Maxime Dénès | 2020-08-28 16:39:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-28 17:24:59 +0200 |
| commit | d1dc6347fb9aa0659f8a8e824c33937d6bfb6e3e (patch) | |
| tree | 18edfe7faf45f41a71845ee8d3f9ae90257e3a93 /engine/evd.mli | |
| parent | 911f33f0a0ff648082d329841388f59e8cecf231 (diff) | |
Enrich `evar_map` printer with future goals stack
This is a useful for debugging.
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index db5265ca0a..5c7a529b9c 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -392,6 +392,8 @@ val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map val remove_future_goal : evar_map -> Evar.t -> evar_map +val pr_future_goals_stack : evar_map -> Pp.t + val give_up : Evar.t -> evar_map -> evar_map val given_up : evar_map -> Evar.Set.t |