Moving printing code from Evd to Termops.

12 files changed, 370 insertions, 334 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 04aacdc09..33fc52e20 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,9 +165,9 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
-let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
-let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
+let ppmetas metas = pp(Termops.pr_metaset metas)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
@@ -178,14 +178,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
-let ppgoalsigma g = pp(Printer.pr_goal g ++ pr_evar_map None (Refiner.project g))
+let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g))
 let pphintdb db = pp(Hints.pr_hint_db db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
-  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ pr_evar_map (Some 1) sigma)
+  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (pr_evar_map (Some 2) evd ++ pr_constr c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)
@@ -215,7 +215,7 @@ let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
 let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
 let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
-let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l)
+let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l)
 let ppconstraints c = pp (pr_constraints Level.pr c)
 let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
diff --git a/engine/evd.ml b/engine/evd.ml
index b30702d0d..3f00b91b6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -258,7 +258,6 @@ type evar_universe_context = UState.t
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
 let empty_evar_universe_context = UState.empty
-let is_empty_evar_universe_context = UState.is_empty
 let union_evar_universe_context = UState.union
 let evar_universe_context_set = UState.context_set
 let evar_universe_context_constraints = UState.constraints
@@ -505,15 +504,6 @@ let find_undefined d e = EvMap.find e d.undf_evars
 
 let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
 
-(* spiwack: this function loses information from the original evar_map
-   it might be an idea not to export it. *)
-let to_list d =
-  (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
-  let l = ref [] in
-  EvMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars;
-  EvMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars;
-  !l
-
 let undefined_map d = d.undf_evars
 
 let drop_all_defined d = { d with defn_evars = EvMap.empty }
@@ -766,7 +756,6 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = UState.context_set d.universes
 
-let pr_uctx_level = UState.pr_uctx_level
 let universe_context ?names evd = UState.universe_context ?names evd.universes
 
 let restrict_universe_context evd vars =
@@ -1178,280 +1167,3 @@ module Monad =
 (* Failure explanation *)
 
 type unsolvability_explanation = SeveralInstancesFound of int
-
-(**********************************************************)
-(* Pretty-printing *)
-
-let pr_evar_suggested_name evk sigma =
-  let base_id evk' evi =
-  match evar_ident evk' sigma with
-  | Some id -> id
-  | None -> match evi.evar_source with
-  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
-  | _,Evar_kinds.VarInstance id -> id
-  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
-  | _ ->
-      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
-  in
-  let names = EvMap.mapi base_id sigma.undf_evars in
-  let id = EvMap.find evk names in
-  let fold evk' id' (seen, n) =
-    if seen then (seen, n)
-    else if Evar.equal evk evk' then (true, n)
-    else if Id.equal id id' then (seen, succ n)
-    else (seen, n)
-  in
-  let (_, n) = EvMap.fold fold names (false, 0) in
-  if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
-
-let pr_existential_key sigma evk = match evar_ident evk sigma with
-| None ->
-  str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
-| Some id ->
-  str "?" ++ pr_id id
-
-let pr_instance_status (sc,typ) =
-  begin match sc with
-  | IsSubType -> str " [or a subtype of it]"
-  | IsSuperType -> str " [or a supertype of it]"
-  | Conv -> mt ()
-  end ++
-  begin match typ with
-  | CoerceToType -> str " [up to coercion]"
-  | TypeNotProcessed -> mt ()
-  | TypeProcessed -> str " [type is checked]"
-  end
-
-let protect f x =
-  try f x
-  with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
-
-let (f_print_constr, print_constr_hook) = Hook.make ()
-
-let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) empty c) a
-
-let pr_meta_map mmap =
-  let pr_name = function
-      Name id -> str"[" ++ pr_id id ++ str"]"
-    | _ -> mt() in
-  let pr_meta_binding = function
-    | (mv,Cltyp (na,b)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " : " ++
-           print_constr b.rebus ++ fnl ())
-    | (mv,Clval(na,(b,s),t)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " := " ++
-           print_constr b.rebus ++
-	   str " : " ++ print_constr t.rebus ++
-	   spc () ++ pr_instance_status s ++ fnl ())
-  in
-  prlist pr_meta_binding (metamap_to_list mmap)
-
-let pr_decl (decl,ok) =
-  match decl with
-  | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
-  | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
-                           print_constr c ++ str (if ok then ")" else "}")
-
-let pr_evar_source = function
-  | Evar_kinds.QuestionMark _ -> str "underscore"
-  | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
-  | Evar_kinds.CasesType true ->
-      str "subterm of pattern-matching return predicate"
-  | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
-  | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
-  | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
-      let id = Option.get ido in
-      str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
-      spc () ++ print_constr (printable_constr_of_global c)
-  | Evar_kinds.InternalHole -> str "internal placeholder"
-  | Evar_kinds.TomatchTypeParameter (ind,n) ->
-      pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
-  | Evar_kinds.GoalEvar -> str "goal evar"
-  | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
-  | Evar_kinds.MatchingVar _ -> str "matching variable"
-  | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
-  | Evar_kinds.SubEvar evk ->
-      str "subterm of " ++ str (string_of_existential evk)
-
-let pr_evar_info evi =
-  let phyps =
-    try
-      let decls = match Filter.repr (evar_filter evi) with
-      | None -> List.map (fun c -> (c, true)) (evar_context evi)
-      | Some filter -> List.combine (evar_context evi) filter
-      in
-      prlist_with_sep spc pr_decl (List.rev decls)
-    with Invalid_argument _ -> str "Ill-formed filtered context" in
-  let pty = print_constr evi.evar_concl in
-  let pb =
-    match evi.evar_body with
-      | Evar_empty -> mt ()
-      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
-  in
-  let candidates =
-    match evi.evar_body, evi.evar_candidates with
-      | Evar_empty, Some l ->
-           spc () ++ str "{" ++
-           prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
-      | _ ->
-          mt ()
-  in
-  let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
-  hov 2
-    (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]" ++
-       candidates ++ spc() ++ src)
-
-let compute_evar_dependency_graph (sigma : evar_map) =
-  (* Compute the map binding ev to the evars whose body depends on ev *)
-  let fold evk evi acc =
-    let fold_ev evk' acc =
-      let tab =
-        try EvMap.find evk' acc
-        with Not_found -> Evar.Set.empty
-      in
-      EvMap.add evk' (Evar.Set.add evk tab) acc
-    in
-    match evar_body evi with
-    | Evar_empty -> assert false
-    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
-  in
-  EvMap.fold fold sigma.defn_evars EvMap.empty
-
-let evar_dependency_closure n sigma =
-  (** Create the DAG of depth [n] representing the recursive dependencies of
-      undefined evars. *)
-  let graph = compute_evar_dependency_graph sigma in
-  let rec aux n curr accu =
-    if Int.equal n 0 then Evar.Set.union curr accu
-    else
-      let fold evk accu =
-        try
-          let deps = EvMap.find evk graph in
-          Evar.Set.union deps accu
-        with Not_found -> accu
-      in
-      (** Consider only the newly added evars *)
-      let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
-      (** Merge the others *)
-      let accu = Evar.Set.union curr accu in
-      aux (n - 1) ncurr accu
-  in
-  let undef = EvMap.domain (undefined_map sigma) in
-  aux n undef Evar.Set.empty
-
-let evar_dependency_closure n sigma =
-  let deps = evar_dependency_closure n sigma in
-  let map = EvMap.bind (fun ev -> find sigma ev) deps in
-  EvMap.bindings map
-
-let has_no_evar sigma =
-  EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
-
-let pr_evd_level evd = pr_uctx_level evd.universes
-
-let pr_evar_universe_context ctx =
-  let prl = pr_uctx_level ctx in
-  if is_empty_evar_universe_context ctx then mt ()
-  else
-    (str"UNIVERSES:"++brk(0,1)++ 
-       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
-     str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
-     h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
-     str"UNDEFINED UNIVERSES:"++brk(0,1)++
-       h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
-
-let print_env_short env =
-  let pr_rel_decl = function
-    | RelDecl.LocalAssum (n,_) -> pr_name n
-    | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
-  in
-  let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
-  let nc = List.rev (named_context env) in
-  let rc = List.rev (rel_context env) in
-    str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
-    str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
-
-let pr_evar_constraints pbs =
-  let pr_evconstr (pbty, env, t1, t2) =
-    let env =
-      (** We currently allow evar instances to refer to anonymous de
-          Bruijn indices, so we protect the error printing code in this
-          case by giving names to every de Bruijn variable in the
-          rel_context of the conversion problem. MS: we should rather
-          stop depending on anonymous variables, they can be used to
-          indicate independency. Also, this depends on a strategy for
-          naming/renaming. *)
-      Namegen.make_all_name_different env
-    in
-    print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      Hook.get f_print_constr env empty t1 ++ spc () ++
-      str (match pbty with
-            | Reduction.CONV -> "=="
-            | Reduction.CUMUL -> "<=") ++
-      spc () ++ Hook.get f_print_constr env empty t2
-  in
-  prlist_with_sep fnl pr_evconstr pbs
-
-let pr_evar_map_gen with_univs pr_evars sigma =
-  let { universes = uvs } = sigma in
-  let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
-  and svs = if with_univs then pr_evar_universe_context uvs else mt ()
-  and cstrs =
-    if List.is_empty sigma.conv_pbs then mt ()
-    else
-    str "CONSTRAINTS:" ++ brk (0, 1) ++
-      pr_evar_constraints sigma.conv_pbs ++ fnl ()
-  and metas =
-    if Metamap.is_empty sigma.metas then mt ()
-    else
-      str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma.metas
-  in
-  evs ++ svs ++ cstrs ++ metas
-
-let pr_evar_list sigma l =
-  let pr (ev, evi) =
-    h 0 (str (string_of_existential ev) ++
-      str "==" ++ pr_evar_info evi ++
-      (if evi.evar_body == Evar_empty
-       then str " {" ++  pr_existential_key sigma ev ++ str "}"
-       else mt ()))
-  in
-  h 0 (prlist_with_sep fnl pr l)
-
-let pr_evar_by_depth depth sigma = match depth with
-| None ->
-  (* Print all evars *)
-  str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
-| Some n ->
-  (* Print all evars *)
-  str"UNDEFINED EVARS:"++
-  (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
-  brk(0,1)++
-  pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
-
-let pr_evar_by_filter filter sigma =
-  let defined = Evar.Map.filter filter sigma.defn_evars in
-  let undefined = Evar.Map.filter filter sigma.undf_evars in
-  let prdef =
-    if Evar.Map.is_empty defined then mt ()
-    else str "DEFINED EVARS:" ++ brk (0, 1) ++
-      pr_evar_list sigma (Evar.Map.bindings defined)
-  in
-  let prundef =
-    if Evar.Map.is_empty undefined then mt ()
-    else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
-      pr_evar_list sigma (Evar.Map.bindings undefined)
-  in
-  prdef ++ prundef
-
-let pr_evar_map ?(with_univs=true) depth sigma =
-  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
-
-let pr_evar_map_filter ?(with_univs=true) filter sigma =
-  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
-
-let pr_metaset metas =
-  str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]"
diff --git a/engine/evd.mli b/engine/evd.mli
index eeb9fd861..fc1d4a514 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -584,22 +584,6 @@ type open_constr = evar_map * constr (* Special case when before is empty *)
 type unsolvability_explanation = SeveralInstancesFound of int
 (** Failure explanation. *)
 
-val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
-
-val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
-
-(** {5 Debug pretty-printers} *)
-
-val print_constr_hook : (Environ.env -> evar_map -> constr -> Pp.std_ppcmds) Hook.t
-val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
-val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
-val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
-  evar_map -> Pp.std_ppcmds
-val pr_metaset : Metaset.t -> Pp.std_ppcmds
-val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
-val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
-
 (** {5 Deprecated functions} *)
 
 val create_evar_defs      : evar_map -> evar_map
diff --git a/engine/termops.ml b/engine/termops.ml
index c35e92f97..ff1a0d9de 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -101,7 +101,329 @@ let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr
 let print_constr_env env sigma t = !term_printer env sigma t
 let print_constr t = !term_printer (Global.env()) Evd.empty t
 let set_print_constr f = term_printer := f
-let () = Hook.set Evd.print_constr_hook (fun env sigma c -> !term_printer env sigma (EConstr.of_constr c))
+
+module EvMap = Evar.Map
+
+let pr_evar_suggested_name evk sigma =
+  let open Evd in
+  let base_id evk' evi =
+  match evar_ident evk' sigma with
+  | Some id -> id
+  | None -> match evi.evar_source with
+  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+  | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+  | _ ->
+      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+  in
+  let names = EvMap.mapi base_id (undefined_map sigma) in
+  let id = EvMap.find evk names in
+  let fold evk' id' (seen, n) =
+    if seen then (seen, n)
+    else if Evar.equal evk evk' then (true, n)
+    else if Id.equal id id' then (seen, succ n)
+    else (seen, n)
+  in
+  let (_, n) = EvMap.fold fold names (false, 0) in
+  if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
+
+let pr_existential_key sigma evk =
+let open Evd in
+match evar_ident evk sigma with
+| None ->
+  str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
+| Some id ->
+  str "?" ++ pr_id id
+
+let pr_instance_status (sc,typ) =
+  let open Evd in
+  begin match sc with
+  | IsSubType -> str " [or a subtype of it]"
+  | IsSuperType -> str " [or a supertype of it]"
+  | Conv -> mt ()
+  end ++
+  begin match typ with
+  | CoerceToType -> str " [up to coercion]"
+  | TypeNotProcessed -> mt ()
+  | TypeProcessed -> str " [type is checked]"
+  end
+
+let protect f x =
+  try f x
+  with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+
+let print_kconstr a =
+  protect (fun c -> print_constr (EConstr.of_constr c)) a
+
+let pr_meta_map evd =
+  let open Evd in
+  let print_constr = print_kconstr in
+  let pr_name = function
+      Name id -> str"[" ++ pr_id id ++ str"]"
+    | _ -> mt() in
+  let pr_meta_binding = function
+    | (mv,Cltyp (na,b)) ->
+      	hov 0
+	  (pr_meta mv ++ pr_name na ++ str " : " ++
+           print_constr b.rebus ++ fnl ())
+    | (mv,Clval(na,(b,s),t)) ->
+      	hov 0
+	  (pr_meta mv ++ pr_name na ++ str " := " ++
+           print_constr b.rebus ++
+	   str " : " ++ print_constr t.rebus ++
+	   spc () ++ pr_instance_status s ++ fnl ())
+  in
+  prlist pr_meta_binding (meta_list evd)
+
+let pr_decl (decl,ok) =
+  let open NamedDecl in
+  let print_constr = print_kconstr in
+  match decl with
+  | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
+  | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
+                           print_constr c ++ str (if ok then ")" else "}")
+
+let pr_evar_source = function
+  | Evar_kinds.QuestionMark _ -> str "underscore"
+  | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
+  | Evar_kinds.CasesType true ->
+      str "subterm of pattern-matching return predicate"
+  | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id
+  | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+  | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
+      let open Globnames in
+      let print_constr = print_kconstr in
+      let id = Option.get ido in
+      str "parameter " ++ pr_id id ++ spc () ++ str "of" ++
+      spc () ++ print_constr (printable_constr_of_global c)
+  | Evar_kinds.InternalHole -> str "internal placeholder"
+  | Evar_kinds.TomatchTypeParameter (ind,n) ->
+      let print_constr = print_kconstr in
+      pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+  | Evar_kinds.GoalEvar -> str "goal evar"
+  | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
+  | Evar_kinds.MatchingVar _ -> str "matching variable"
+  | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id
+  | Evar_kinds.SubEvar evk ->
+      let open Evd in
+      str "subterm of " ++ str (string_of_existential evk)
+
+let pr_evar_info evi =
+  let open Evd in
+  let print_constr = print_kconstr in
+  let phyps =
+    try
+      let decls = match Filter.repr (evar_filter evi) with
+      | None -> List.map (fun c -> (c, true)) (evar_context evi)
+      | Some filter -> List.combine (evar_context evi) filter
+      in
+      prlist_with_sep spc pr_decl (List.rev decls)
+    with Invalid_argument _ -> str "Ill-formed filtered context" in
+  let pty = print_constr evi.evar_concl in
+  let pb =
+    match evi.evar_body with
+      | Evar_empty -> mt ()
+      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
+  in
+  let candidates =
+    match evi.evar_body, evi.evar_candidates with
+      | Evar_empty, Some l ->
+           spc () ++ str "{" ++
+           prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
+      | _ ->
+          mt ()
+  in
+  let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
+  hov 2
+    (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]" ++
+       candidates ++ spc() ++ src)
+
+let compute_evar_dependency_graph sigma =
+  let open Evd in
+  (* Compute the map binding ev to the evars whose body depends on ev *)
+  let fold evk evi acc =
+    let fold_ev evk' acc =
+      let tab =
+        try EvMap.find evk' acc
+        with Not_found -> Evar.Set.empty
+      in
+      EvMap.add evk' (Evar.Set.add evk tab) acc
+    in
+    match evar_body evi with
+    | Evar_empty -> acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
+  in
+  Evd.fold fold sigma EvMap.empty
+
+let evar_dependency_closure n sigma =
+  let open Evd in
+  (** Create the DAG of depth [n] representing the recursive dependencies of
+      undefined evars. *)
+  let graph = compute_evar_dependency_graph sigma in
+  let rec aux n curr accu =
+    if Int.equal n 0 then Evar.Set.union curr accu
+    else
+      let fold evk accu =
+        try
+          let deps = EvMap.find evk graph in
+          Evar.Set.union deps accu
+        with Not_found -> accu
+      in
+      (** Consider only the newly added evars *)
+      let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
+      (** Merge the others *)
+      let accu = Evar.Set.union curr accu in
+      aux (n - 1) ncurr accu
+  in
+  let undef = EvMap.domain (undefined_map sigma) in
+  aux n undef Evar.Set.empty
+
+let evar_dependency_closure n sigma =
+  let open Evd in
+  let deps = evar_dependency_closure n sigma in
+  let map = EvMap.bind (fun ev -> find sigma ev) deps in
+  EvMap.bindings map
+
+let has_no_evar sigma =
+  try let () = Evd.fold (fun _ _ () -> raise Exit) sigma () in true
+  with Exit -> false
+
+let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
+
+let pr_evar_universe_context ctx =
+  let open UState in
+  let open Evd in
+  let prl = pr_uctx_level ctx in
+  if UState.is_empty ctx then mt ()
+  else
+    (str"UNIVERSES:"++brk(0,1)++ 
+       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
+     str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
+     h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
+     str"UNDEFINED UNIVERSES:"++brk(0,1)++
+       h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
+
+let print_env_short env =
+  let print_constr = print_kconstr in
+  let pr_rel_decl = function
+    | RelDecl.LocalAssum (n,_) -> pr_name n
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+  in
+  let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
+  let nc = List.rev (named_context env) in
+  let rc = List.rev (rel_context env) in
+    str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
+    str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
+
+let pr_evar_constraints pbs =
+  let pr_evconstr (pbty, env, t1, t2) =
+    let env =
+      (** We currently allow evar instances to refer to anonymous de
+          Bruijn indices, so we protect the error printing code in this
+          case by giving names to every de Bruijn variable in the
+          rel_context of the conversion problem. MS: we should rather
+          stop depending on anonymous variables, they can be used to
+          indicate independency. Also, this depends on a strategy for
+          naming/renaming. *)
+      Namegen.make_all_name_different env
+    in
+    print_env_short env ++ spc () ++ str "|-" ++ spc () ++
+      print_constr_env env Evd.empty (EConstr.of_constr t1) ++ spc () ++
+      str (match pbty with
+            | Reduction.CONV -> "=="
+            | Reduction.CUMUL -> "<=") ++
+      spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2)
+  in
+  prlist_with_sep fnl pr_evconstr pbs
+
+let pr_evar_map_gen with_univs pr_evars sigma =
+  let uvs = Evd.evar_universe_context sigma in
+  let (_, conv_pbs) = Evd.extract_all_conv_pbs sigma in
+  let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
+  and svs = if with_univs then pr_evar_universe_context uvs else mt ()
+  and cstrs =
+    if List.is_empty conv_pbs then mt ()
+    else
+    str "CONSTRAINTS:" ++ brk (0, 1) ++
+      pr_evar_constraints conv_pbs ++ 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
+
+let pr_evar_list sigma l =
+  let open Evd in
+  let pr (ev, evi) =
+    h 0 (str (string_of_existential ev) ++
+      str "==" ++ pr_evar_info evi ++
+      (if evi.evar_body == Evar_empty
+       then str " {" ++  pr_existential_key sigma ev ++ str "}"
+       else mt ()))
+  in
+  h 0 (prlist_with_sep fnl pr l)
+
+let pr_evar_by_depth depth sigma = match depth with
+| None ->
+  (* Print all evars *)
+  let to_list d =
+    let open Evd in
+    (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
+    let l = ref [] in
+    let fold_def evk evi () = match evi.evar_body with
+    | Evar_defined _ -> l := (evk, evi) :: !l
+    | Evar_empty -> ()
+    in
+    let fold_undef evk evi () = match evi.evar_body with
+    | Evar_empty -> l := (evk, evi) :: !l
+    | Evar_defined _ -> ()
+    in
+    Evd.fold fold_def d ();
+    Evd.fold fold_undef d ();
+    !l
+  in
+  str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
+| Some n ->
+  (* Print all evars *)
+  str"UNDEFINED EVARS:"++
+  (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
+  brk(0,1)++
+  pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
+
+let pr_evar_by_filter filter sigma =
+  let open Evd in
+  let elts = Evd.fold (fun evk evi accu -> (evk, evi) :: accu) sigma [] in
+  let elts = List.rev elts in
+  let is_def (_, evi) = match evi.evar_body with
+  | Evar_defined _ -> true
+  | Evar_empty -> false
+  in
+  let (defined, undefined) = List.partition is_def elts in
+  let filter (evk, evi) = filter evk evi in
+  let defined = List.filter filter defined in
+  let undefined = List.filter filter undefined in
+  let prdef =
+    if List.is_empty defined then mt ()
+    else str "DEFINED EVARS:" ++ brk (0, 1) ++
+      pr_evar_list sigma defined
+  in
+  let prundef =
+    if List.is_empty undefined then mt ()
+    else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
+      pr_evar_list sigma undefined
+  in
+  prdef ++ prundef
+
+let pr_evar_map ?(with_univs=true) depth sigma =
+  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
+
+let pr_evar_map_filter ?(with_univs=true) filter sigma =
+  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
+
+let pr_metaset metas =
+  str "[" ++ pr_sequence pr_meta (Evd.Metaset.elements metas) ++ str "]"
 
 let pr_var_decl env decl =
   let open NamedDecl in
diff --git a/engine/termops.mli b/engine/termops.mli
index 841de34b1..512bb05ff 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -20,15 +20,6 @@ val print_sort : sorts -> std_ppcmds
 val pr_sort_family : sorts_family -> std_ppcmds
 val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds
 
-(** debug printer: do not use to display terms to the casual user... *)
-val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
-val print_constr     : constr -> std_ppcmds
-val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds
-val print_named_context : env -> std_ppcmds
-val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
-val print_rel_context : env -> std_ppcmds
-val print_env : env -> std_ppcmds
-
 (** about contexts *)
 val push_rel_assum : Name.t * types -> env -> env
 val push_rels_assum : (Name.t * Constr.types) list -> env -> env
@@ -287,3 +278,30 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 (** {6 Functions to deal with impossible cases } *)
 val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
 val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
+
+(** {5 Debug pretty-printers} *)
+
+open Evd
+
+val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+
+val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+
+val pr_evar_info : evar_info -> Pp.std_ppcmds
+val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
+val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
+val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
+  evar_map -> Pp.std_ppcmds
+val pr_metaset : Metaset.t -> Pp.std_ppcmds
+val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
+val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
+
+(** debug printer: do not use to display terms to the casual user... *)
+
+val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
+val print_constr     : constr -> std_ppcmds
+val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds
+val print_named_context : env -> std_ppcmds
+val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
+val print_rel_context : env -> std_ppcmds
+val print_env : env -> std_ppcmds
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index b45ead217..bc57fcf56 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1511,7 +1511,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 	   if not (Evd.is_defined acc ev) then 
 	     user_err ~hdr:"rewrite"
 			  (str "Unsolved constraint remaining: " ++ spc () ++
-			   Evd.pr_evar_info (Evd.find acc ev))
+			   Termops.pr_evar_info (Evd.find acc ev))
 	   else Evd.remove acc ev) 
 	  cstrs evars'
       in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d4e156fa4..c8d945c0b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -422,7 +422,7 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
+       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -434,7 +434,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
+  GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
 
 let detype_instance sigma l = 
   if Univ.Instance.is_empty l then None
@@ -533,7 +533,7 @@ let rec detype flags avoid env sigma t =
       let id,l =
         try
           let id = match Evd.evar_ident evk sigma with
-          | None -> Evd.pr_evar_suggested_name evk sigma
+          | None -> Termops.pr_evar_suggested_name evk sigma
           | Some id -> id
           in
           let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
diff --git a/printing/printer.ml b/printing/printer.ml
index d9060c172..c7d3a1ba3 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -223,7 +223,7 @@ let safe_pr_constr t =
 let pr_universe_ctx sigma c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c
+      (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c
   else
     mt()
 
@@ -240,7 +240,7 @@ let pr_puniverses f env (c,u) =
    else mt ())
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
-let pr_existential_key = Evd.pr_existential_key
+let pr_existential_key = Termops.pr_existential_key
 let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
 let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
 let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
@@ -922,4 +922,4 @@ let pr_polymorphic b =
 
 let pr_universe_instance evd ctx =
   let inst = Univ.UContext.instance ctx in
-    str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
+    str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 1ddb67edd..59a41792a 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -58,6 +58,6 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err ~loc 
                 (str "Instance is not well-typed in the environment of " ++
-                 pr_existential_key sigma evk ++ str ".")
+                 Termops.pr_existential_key sigma evk ++ str ".")
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/stm/stm.ml b/stm/stm.ml
index 47e806929..6f5da37f4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1791,7 +1791,7 @@ end = struct (* {{{ *)
             prerr_endline (fun () -> string_of_ppcmds(hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
-              str"uc=" ++ Evd.pr_evar_universe_context uc)));
+              str"uc=" ++ Termops.pr_evar_universe_context uc)));
             (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
               (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
               Tactics.exact_no_check (EConstr.of_constr pt))
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 50301ee0d..6982205fd 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -691,7 +691,7 @@ let explain_non_linear_unification env sigma m t =
 
 let explain_unsatisfied_constraints env sigma cst =
   strbrk "Unsatisfied constraints: " ++ 
-    Univ.pr_constraints (Evd.pr_evd_level sigma) cst ++ 
+    Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++ 
     spc () ++ str "(maybe a bugged tactic)."
 
 let explain_type_error env sigma err =
@@ -903,7 +903,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
-      quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst)
+      quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
   str "Signature components for label " ++ pr_label l ++
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f3d73b76c..55477cbcf 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -81,8 +81,8 @@ let show_universes () =
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
-    Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
-    Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
+    Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
+    Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
 
 let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)