diff options
| author | Pierre-Marie Pédrot | 2018-10-27 14:04:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-27 14:04:32 +0200 |
| commit | 788ff535ed27d5142cd18878f8478bfc161945cd (patch) | |
| tree | cd513a51eaaa0ed5552c319cdc38b875bf7f2abc /engine/termops.ml | |
| parent | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (diff) | |
| parent | fb1c2a017ef8112e061771db14ccc6cc1f09d41c (diff) | |
Merge PR #8741: [typeclasses] functionalize typeclass evar handling
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..5e220fd8f1 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 typeclasses = + let evars = Evd.get_typeclass_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "TYPECLASSES:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (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 ++ typeclasses ++ metas let pr_evar_list sigma l = let open Evd in |