diff options
| author | Matthieu Sozeau | 2018-10-08 02:14:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-26 18:29:36 +0200 |
| commit | 9f65b8bf9775dd571a806e10ac356b1b8f8ae2c5 (patch) | |
| tree | 56a49e0cd7d6ee19d4bb25ff0165e1c1466a7e73 /engine/termops.ml | |
| parent | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (diff) | |
Cleanup evar_extra: remove evar_info's store and add maps to evar_map
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index e1f5fb0d7f..c4b57e4dd2 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -365,12 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma = else str "CONSTRAINTS:" ++ brk (0, 1) ++ pr_evar_constraints sigma conv_pbs ++ fnl () + and unresolvables = + let evars = Evd.unresolvable_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "UNRESOLVABLE:" ++ brk (0, 1) ++ + prlist_with_sep spc (pr_existential_key sigma) (Evar.Set.elements evars) ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma in - evs ++ svs ++ cstrs ++ metas + evs ++ svs ++ cstrs ++ unresolvables ++ metas let pr_evar_list sigma l = let open Evd in |