diff options
| author | Pierre-Marie Pédrot | 2020-08-30 00:11:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-30 00:11:07 +0200 |
| commit | 94d9fe2b6cb06fe7f862683d8337433e18314001 (patch) | |
| tree | 34fa326053596691829658d29c93f6e74ece0eb1 /engine/termops.ml | |
| parent | fd8da75905aac60d9c38eb0369a3cd10081ce586 (diff) | |
| parent | d1dc6347fb9aa0659f8a8e824c33937d6bfb6e3e (diff) | |
Merge PR #12934: Enrich `evar_map` printer with future goals stack
Reviewed-by: ppedrot
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index e5231ef9cd..7579631313 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -301,8 +301,10 @@ let pr_evar_map_gen with_univs pr_evars env sigma = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma + and future_goals = + str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl () in - evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ future_goals let pr_evar_list env sigma l = let open Evd in |