6 files changed, 37 insertions, 38 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 710743e92d..efe1525c9a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -22,6 +22,8 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
+module Internal = struct
+
 (* Sorts and sort family *)
 
 let print_sort = function
@@ -98,12 +100,16 @@ let rec pr_constr c = match kind c with
            cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
-let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
+let term_printer = ref debug_print_constr_env
+
 let print_constr_env env sigma t = !term_printer env sigma t
 let print_constr t =
   let env = Global.env () in
   let evd = Evd.from_env env in
   !term_printer env evd t
+
 let set_print_constr f = term_printer := f
 
 module EvMap = Evar.Map
@@ -1537,3 +1543,6 @@ let env_rel_context_chop k env =
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
   ctx1
+end
+
+include Internal
diff --git a/engine/termops.mli b/engine/termops.mli
index 9ce2db9234..aa0f837938 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -311,18 +311,40 @@ val pr_metaset : Metaset.t -> Pp.t
 val pr_evar_universe_context : UState.t -> Pp.t
 val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
 
-(** Internal hook to register user-level printer *)
+module Internal : sig
 
-val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+(** NOTE: to print terms you always want to use functions in
+   Printer, not these ones which are for very special cases. *)
 
-(** User-level printers *)
+(** debug printers: print raw form for terms, both with
+   evar-substitution and without.  *)
+val debug_print_constr : constr -> Pp.t
+val debug_print_constr_env : env -> evar_map -> constr -> Pp.t
 
-val print_constr     : constr -> Pp.t
+(** Pretty-printer hook: [print_constr_env env sigma c] will pretty
+   print c if the pretty printing layer has been linked into the Coq
+   binary. *)
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
 
-(** debug printer: do not use to display terms to the casual user... *)
+(** [set_print_constr f] sets f to be the pretty printer *)
+val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
 
+(** Printers for contexts *)
 val print_named_context : env -> Pp.t
 val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
 val print_rel_context : env -> Pp.t
 val print_env : env -> Pp.t
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use print_constr_env"]
+
+end
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_rel_context : env -> Pp.t
+[@@deprecated "use Internal.print_rel_context"]
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 9e4c6e47fc..70cdd3a2db 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -11,7 +11,6 @@
 open Util
 open Names
 open Univ
-open Nametab
 
 
 let qualid_of_level l =
@@ -31,20 +30,6 @@ let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
 (** Global universe information outside the kernel, to handle
     polymorphic universe names in sections that have to be discharged. *)
 
-let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
-
-let add_global_universe u p =
-  match Level.name u with
-  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
-  | None -> ()
-
-let is_polymorphic l =
-  match Level.name l with
-  | Some n ->
-     (try Nametab.UnivIdMap.find n !universe_map
-      with Not_found -> false)
-  | None -> false
-
 (** Local universe names of polymorphic references *)
 
 type universe_binders = Univ.Level.t Names.Id.Map.t
diff --git a/engine/univNames.mli b/engine/univNames.mli
index d794d7b744..bd4062ade4 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -13,13 +13,6 @@ open Univ
 val pr_with_global_universes : Level.t -> Pp.t
 val qualid_of_level : Level.t -> Libnames.qualid
 
-(** Global universe information outside the kernel, to handle
-    polymorphic universes in sections that have to be discharged. *)
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-
-(** Is [lvl]  a global polymorphic universe? (ie section polymorphic universe) *)
-val is_polymorphic : Level.t -> bool
-
 (** Local universe name <-> level mapping *)
 
 type universe_binders = Univ.Level.t Names.Id.Map.t
diff --git a/engine/universes.ml b/engine/universes.ml
index c7e5f654a1..5d0157b2db 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -19,10 +19,6 @@ type univ_name_list = UnivNames.univ_name_list
 let pr_with_global_universes = UnivNames.pr_with_global_universes
 let reference_of_level = UnivNames.qualid_of_level
 
-let add_global_universe = UnivNames.add_global_universe
-
-let is_polymorphic = UnivNames.is_polymorphic
-
 let empty_binders = UnivNames.empty_binders
 
 let register_universe_binders = UnivNames.register_universe_binders
diff --git a/engine/universes.mli b/engine/universes.mli
index 7ca33f47a1..0d3bae4c95 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -25,12 +25,6 @@ val pr_with_global_universes : Level.t -> Pp.t
 val reference_of_level : Level.t -> Libnames.qualid
 [@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"]
 
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
-
-val is_polymorphic : Level.t -> bool
-[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"]
-
 type universe_binders = UnivNames.universe_binders
 [@@ocaml.deprecated "Use [UnivNames.universe_binders]"]