Cleanup debug printers a bit, add generated mli.

7 files changed, 146 insertions, 17 deletions

diff --git a/Makefile.build b/Makefile.build
index 940943c41..a9dbc4b44 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -595,11 +595,14 @@ API/API.cmi : API/API.mli
 	$(SHOW)'OCAMLOPT -pack -o $@'
 	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
+COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,)
+COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
+
 COND_BYTEFLAGS= \
- $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS)
+ $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS)
 
 COND_OPTFLAGS= \
- $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS)
+ $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS)
 
 %.cmi: %.mli
 	$(SHOW)'OCAMLC    $<'
diff --git a/dev/base_include b/dev/base_include
index 1da5e3ed1..d6c00ef5a 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -54,7 +54,7 @@
 #install_printer ppvblock;;
 #install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
-#install_printer  (* substitution *) prsubst;;
+#install_printer  (* substitution *) ppsubst;;
 
 (* Open main files *)
 
diff --git a/dev/db b/dev/db
index 24ae3957e..f71645041 100644
--- a/dev/db
+++ b/dev/db
@@ -42,7 +42,6 @@ install_printer Top_printers.ppuniverse_level_subst
 install_printer Top_printers.ppevar_universe_context
 install_printer Top_printers.ppcumulativity_info
 install_printer Top_printers.ppabstract_cumulativity_info
-install_printer Top_printers.pptype
 install_printer Top_printers.ppj
 install_printer Top_printers.ppenv
 install_printer Top_printers.ppnamedcontextval
@@ -59,8 +58,8 @@ install_printer Top_printers.pphintdb
 install_printer Top_printers.pptac
 install_printer Top_printers.ppobj
 install_printer Top_printers.pploc
-install_printer Top_printers.prsubst
-install_printer Top_printers.prdelta
+install_printer Top_printers.ppsubst
+install_printer Top_printers.ppdelta
 install_printer Top_printers.ppfconstr
 install_printer Top_printers.ppgenarginfo
 install_printer Top_printers.ppgenargargt
diff --git a/dev/include b/dev/include
index 0d34595f4..b982f4c9f 100644
--- a/dev/include
+++ b/dev/include
@@ -36,7 +36,6 @@
 #install_printer  (* constraints *)  ppconstraints;;
 #install_printer  (* univ constraints *)  ppuniverseconstraints;;
 #install_printer  (* universe *)  ppuni;;
-#install_printer  (* universes *)  ppuniverse;;
 #install_printer  (* universes *)  ppuniverses;;
 #install_printer  (* univ level *) ppuni_level;;
 #install_printer  (* univ context *) ppuniverse_context;;
diff --git a/dev/set_raw_db b/dev/set_raw_db
deleted file mode 100644
index 5caff7e5d..000000000
--- a/dev/set_raw_db
+++ /dev/null
@@ -1 +0,0 @@
-install_printer Top_printers.ppconstrdb
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 832040ad2..5011bcaff 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -50,13 +50,13 @@ let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Classops.pr_cl_index cl)
 let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
 
-let pprecarg = function
+let prrecarg = function
   | Declarations.Norec -> str "Norec"
   | Declarations.Mrec (mind,i) ->
      str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
   | Declarations.Imbr (mind,i) ->
      str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
-let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
+let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
 
 (* term printers *)
 let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
@@ -65,8 +65,6 @@ let ppevar evk = pp (Evar.print evk)
 let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
 let ppeconstr x = pp (Termops.print_constr x)
 let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
-let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x))
-let ppterm = ppconstr
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
@@ -111,7 +109,7 @@ let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
 let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
 
 let ppunbound_ltac_var_map l = ppidmap (fun _ arg ->
-  str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">")
+  str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") l
 
 open Ltac_pretype
 let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
@@ -149,8 +147,8 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
 let ppj j = pp (genppj (envpp pr_ljudge_env) j)
 
-let prsubst s = pp (Mod_subst.debug_pr_subst s)
-let prdelta s = pp (Mod_subst.debug_pr_delta s)
+let ppsubst s = pp (Mod_subst.debug_pr_subst s)
+let ppdelta s = pp (Mod_subst.debug_pr_delta s)
 
 let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
@@ -200,9 +198,8 @@ let pppftreestate p = pp(print_pftreestate p)
 
 let pproof p = pp(Proof.pr_proof p)
 
-let ppuni u = pp(pr_uni u)
+let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
-let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]")
 
 let prlev = Universes.pr_with_global_universes
 let ppuniverse_set l = pp (LSet.pr prlev l)
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
new file mode 100644
index 000000000..44c0c7365
--- /dev/null
+++ b/dev/top_printers.mli
@@ -0,0 +1,132 @@
+val pp : Pp.t -> unit
+val ppfuture : 'a Future.computation -> unit
+val ppid : Names.Id.t -> unit
+val pplab : Names.Label.t -> unit
+val ppmbid : Names.MBId.t -> unit
+val ppdir : Names.DirPath.t -> unit
+val ppmp : Names.ModPath.t -> unit
+val ppcon : Names.Constant.t -> unit
+val ppproj : Names.Projection.t -> unit
+val ppkn : Names.KerName.t -> unit
+val ppmind : Names.MutInd.t -> unit
+val ppind : Names.MutInd.t * int -> unit
+val ppsp : Libnames.full_path -> unit
+val ppqualid : Libnames.qualid -> unit
+val ppclindex : Classops.cl_index -> unit
+val ppscheme : 'a Ind_tables.scheme_kind -> unit
+val prrecarg : Declarations.recarg -> Pp.t
+val ppwf_paths : Declarations.recarg Rtree.t -> unit
+val envpp : (Environ.env -> Evd.evar_map -> 'a) -> 'a
+val rawdebug : bool ref
+val ppevar : Evar.t -> unit
+val ppconstr : Constr.t -> unit
+val ppeconstr : EConstr.constr -> unit
+val ppconstr_expr : Constrexpr.constr_expr -> unit
+val ppsconstr : Constr.constr Mod_subst.substituted -> unit
+val ppconstr_univ : Constr.t -> unit
+val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
+val pppattern : Pattern.constr_pattern -> unit
+val pptype : Constr.types -> unit
+val ppfconstr : CClosure.fconstr -> unit
+val ppbigint : Bigint.bigint -> unit
+val prset : ('a -> Pp.t) -> 'a list -> Pp.t
+val ppintset : Int.Set.t -> unit
+val ppidset : Names.Id.Set.t -> unit
+val prset' : ('a -> Pp.t) -> 'a list -> Pp.t
+val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t
+val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit
+val pridmapgen : 'a Names.Id.Map.t -> Pp.t
+val ppidmapgen : 'a Names.Id.Map.t -> unit
+val ppevarsubst :
+  (Constr.t * Constr.t option * Names.Id.Map.key) list Names.Id.Map.t -> unit
+val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t
+val ppididmap : Names.Id.t Names.Id.Map.t -> unit
+val prconstrunderbindersidmap :
+  (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> Pp.t
+val ppconstrunderbindersidmap :
+  (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> unit
+val ppunbound_ltac_var_map :
+  'a Genarg.generic_argument Names.Id.Map.t -> unit
+val pr_closure : Ltac_pretype.closure -> Pp.t
+val pr_closed_glob_constr_idmap :
+  Ltac_pretype.closed_glob_constr Names.Id.Map.t -> Pp.t
+val pr_closed_glob_constr : Ltac_pretype.closed_glob_constr -> Pp.t
+val ppclosure : Ltac_pretype.closure -> unit
+val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit
+val ppclosedglobconstridmap :
+  Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit
+val pP : Pp.t -> unit
+val safe_pr_global : Globnames.global_reference -> unit
+val ppglobal : Globnames.global_reference -> unit
+val ppconst :
+  Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit
+val ppvar : Names.Id.t * Constr.constr -> unit
+val genppj : ('a -> Pp.t * Pp.t) -> 'a -> Pp.t
+val ppj : EConstr.unsafe_judgment -> unit
+val ppsubst : Mod_subst.substitution -> unit
+val ppdelta : Mod_subst.delta_resolver -> unit
+val pp_idpred : Names.Id.Pred.t -> unit
+val pp_cpred : Names.Cpred.t -> unit
+val pp_transparent_state : Names.transparent_state -> unit
+val pp_stack_t : Constr.t Reductionops.Stack.t -> unit
+val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit
+val pp_state_t : Reductionops.state -> unit
+val pr_evar : Evar.t -> Pp.t
+val ppmetas : Evd.Metaset.t -> unit
+val ppevm : Evd.evar_map -> unit
+val ppevmall : Evd.evar_map -> unit
+val pr_existentialset : Evar.Set.t -> Pp.t
+val ppexistentialset : Evar.Set.t -> unit
+val ppexistentialfilter : Evd.Filter.t -> unit
+val ppclenv : Clenv.clausenv -> unit
+val ppgoalgoal : Goal.goal -> unit
+val ppgoal : Proof_type.goal Evd.sigma -> unit
+val ppgoalsigma : Proof_type.goal Evd.sigma -> unit
+val pphintdb : Hints.Hint_db.t -> unit
+val ppproofview : Proofview.proofview -> unit
+val ppopenconstr : Evd.open_constr -> unit
+val pproof : Proof.t -> unit
+val ppuni : Univ.Universe.t -> unit
+val ppuni_level : Univ.Level.t -> unit
+val prlev : Univ.Level.t -> Pp.t
+val ppuniverse_set : Univ.LSet.t -> unit
+val ppuniverse_instance : Univ.Instance.t -> unit
+val ppuniverse_context : Univ.UContext.t -> unit
+val ppuniverse_context_set : Univ.ContextSet.t -> unit
+val ppuniverse_subst : Univ.universe_subst -> unit
+val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit
+val ppuniverse_level_subst : Univ.universe_level_subst -> unit
+val ppevar_universe_context : UState.t -> unit
+val ppconstraints : Univ.Constraint.t -> unit
+val ppuniverseconstraints : Universes.Constraints.t -> unit
+val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
+val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
+val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit
+val ppuniverses : UGraph.t -> unit
+val ppnamedcontextval : Environ.named_context_val -> unit
+val ppenv : Environ.env -> unit
+val ppenvwithcst : Environ.env -> unit
+val pptac : Tacexpr.glob_tactic_expr -> unit
+val ppobj : Libobject.obj -> unit
+val cnt : int ref
+val cast_kind_display : Constr.cast_kind -> string
+val constr_display : Constr.constr -> unit
+val print_pure_constr : Constr.types -> unit
+val pploc : Loc.t -> unit
+val pp_argument_type : Genarg.argument_type -> unit
+val pp_generic_argument : 'a Genarg.generic_argument -> unit
+val prgenarginfo : Geninterp.Val.t -> Pp.t
+val ppgenarginfo : Geninterp.Val.t -> unit
+val ppgenargargt : ('a, 'b, 'c) Genarg.ArgT.tag -> unit
+val ppist : Geninterp.interp_sign -> unit
+val in_current_context :
+  (Constr.constr -> 'a) -> Constrexpr.constr_expr -> 'a
+val encode_path :
+  ?loc:Loc.t ->
+  string ->
+  (Names.ModPath.t * Names.DirPath.t) option ->
+  Names.module_ident list -> Names.Id.t -> Libnames.reference
+val raw_string_of_ref :
+  ?loc:Loc.t -> 'a -> Globnames.global_reference -> Libnames.reference
+val short_string_of_ref :
+  ?loc:Loc.t -> 'a -> Globnames.global_reference -> Libnames.reference