From 87cbd64254f33439882156d9a297a6a2f6886057 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 16 Dec 2017 10:58:52 +0100 Subject: Cleanup debug printers a bit, add generated mli. --- dev/base_include | 2 +- dev/db | 5 +- dev/include | 1 - dev/set_raw_db | 1 - dev/top_printers.ml | 15 +++--- dev/top_printers.mli | 132 +++++++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 141 insertions(+), 15 deletions(-) delete mode 100644 dev/set_raw_db create mode 100644 dev/top_printers.mli (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index 1da5e3ed18..d6c00ef5ad 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 24ae3957ef..f716450413 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 0d34595f4f..b982f4c9fa 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 5caff7e5d4..0000000000 --- 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 832040ad2c..5011bcaff6 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"") + 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 0000000000..44c0c7365b --- /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 -- cgit v1.2.3 From 871272d959ac8f2b528cac3677230f2eb33a78c4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 16 Dec 2017 11:00:36 +0100 Subject: Cleanup top_printers.mli --- dev/top_printers.mli | 99 +++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 70 insertions(+), 29 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 44c0c7365b..7b5e4a0b64 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -1,5 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val pP : Pp.t -> unit (* with surrounding box *) + val ppfuture : 'a Future.computation -> unit + val ppid : Names.Id.t -> unit val pplab : Names.Label.t -> unit val ppmbid : Names.MBId.t -> unit @@ -9,44 +22,60 @@ 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 ppind : Names.inductive -> 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 pr_evar : Evar.t -> Pp.t 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 + +(* Multiple printers for Constr.t *) +val ppconstr : Constr.t -> unit (* by Termops printer *) val ppconstr_univ : Constr.t -> unit + +(* Extern as type *) +val pptype : Constr.types -> unit + +val ppsconstr : Constr.constr Mod_subst.substituted -> unit +val ppeconstr : EConstr.constr -> unit (* Termops printer *) +val ppconstr_expr : Constrexpr.constr_expr -> 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 ppevarsubst : + (Constr.t * Constr.t option * Names.Id.Map.key) list 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 @@ -55,40 +84,54 @@ 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 +(* also print evar map *) 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 + +(* Universes *) val ppuni : Univ.Universe.t -> unit -val ppuni_level : Univ.Level.t -> unit -val prlev : Univ.Level.t -> Pp.t +val ppuni_level : Univ.Level.t -> unit (* raw *) +val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *) val ppuniverse_set : Univ.LSet.t -> unit val ppuniverse_instance : Univ.Instance.t -> unit val ppuniverse_context : Univ.UContext.t -> unit @@ -103,30 +146,28 @@ 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 + +(* Some super raw printers *) 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 -- cgit v1.2.3 From 897b37129850002953be4426ffc852da63c8f4e6 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 22 Dec 2017 16:31:20 +0100 Subject: Reorder dev/db --- dev/db | 73 +++++++++++++++++++++++++++++++----------------------------------- 1 file changed, 34 insertions(+), 39 deletions(-) (limited to 'dev') diff --git a/dev/db b/dev/db index f716450413..0f532e3691 100644 --- a/dev/db +++ b/dev/db @@ -2,36 +2,49 @@ source core.dbg load_printer top_printers.cmo install_printer Top_printers.ppfuture - install_printer Top_printers.ppid -install_printer Top_printers.ppidset -install_printer Top_printers.ppevar -install_printer Top_printers.ppevarsubst -install_printer Top_printers.ppexistentialfilter -install_printer Top_printers.ppexistentialset -install_printer Top_printers.ppintset install_printer Top_printers.pplab -install_printer Top_printers.ppdir install_printer Top_printers.ppmbid +install_printer Top_printers.ppdir install_printer Top_printers.ppmp -install_printer Top_printers.ppkn install_printer Top_printers.ppcon -install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppkn install_printer Top_printers.ppmind install_printer Top_printers.ppsp install_printer Top_printers.ppqualid install_printer Top_printers.ppclindex -install_printer Top_printers.ppbigint -install_printer Top_printers.pp_transparent_state - -install_printer Top_printers.pppattern -install_printer Top_printers.ppglob_constr - +install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppevar install_printer Top_printers.ppconstr install_printer Top_printers.ppeconstr +install_printer Top_printers.ppglob_constr +install_printer Top_printers.pppattern +install_printer Top_printers.ppfconstr +install_printer Top_printers.ppbigint +install_printer Top_printers.ppintset +install_printer Top_printers.ppidset +install_printer Top_printers.ppidmapgen +install_printer Top_printers.ppididmap +install_printer Top_printers.ppconstrunderbindersidmap +install_printer Top_printers.ppevarsubst +install_printer Top_printers.ppunbound_ltac_var_map +install_printer Top_printers.ppclosure +install_printer Top_printers.ppclosedglobconstr +install_printer Top_printers.ppj +install_printer Top_printers.ppsubst +install_printer Top_printers.ppdelta +install_printer Top_printers.pp_transparent_state +install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t +install_printer Top_printers.ppmetas +install_printer Top_printers.ppevm +install_printer Top_printers.ppexistentialset +install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppgoalgoal +install_printer Top_printers.ppgoal +install_printer Top_printers.pphintdb +install_printer Top_printers.ppproofview install_printer Top_printers.ppuni -install_printer Top_printers.ppuniverses -install_printer Top_printers.ppconstraints install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context @@ -40,33 +53,15 @@ install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst install_printer Top_printers.ppuniverse_level_subst install_printer Top_printers.ppevar_universe_context +install_printer Top_printers.ppconstraints install_printer Top_printers.ppcumulativity_info install_printer Top_printers.ppabstract_cumulativity_info -install_printer Top_printers.ppj -install_printer Top_printers.ppenv +install_printer Top_printers.ppuniverses install_printer Top_printers.ppnamedcontextval -install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t - -install_printer Top_printers.ppmetas -install_printer Top_printers.ppevm -install_printer Top_printers.ppgoalgoal -install_printer Top_printers.ppgoal -install_printer Top_printers.ppproofview -install_printer Top_printers.pphintdb - +install_printer Top_printers.ppenv install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc -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 install_printer Top_printers.ppist -install_printer Top_printers.ppconstrunderbindersidmap -install_printer Top_printers.ppunbound_ltac_var_map -install_printer Top_printers.ppididmap -install_printer Top_printers.ppidmapgen -install_printer Top_printers.ppclosure -install_printer Top_printers.ppclosedglobconstr -- cgit v1.2.3 From 7b9f83224e13b21fcb5bd1b3742f52070c3299e4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 22 Dec 2017 16:35:22 +0100 Subject: Add printers to dev/db --- dev/db | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'dev') diff --git a/dev/db b/dev/db index 0f532e3691..2f8c13485a 100644 --- a/dev/db +++ b/dev/db @@ -1,6 +1,7 @@ source core.dbg load_printer top_printers.cmo +install_printer Top_printers.pP install_printer Top_printers.ppfuture install_printer Top_printers.ppid install_printer Top_printers.pplab @@ -8,15 +9,20 @@ install_printer Top_printers.ppmbid install_printer Top_printers.ppdir install_printer Top_printers.ppmp install_printer Top_printers.ppcon +install_printer Top_printers.ppproj install_printer Top_printers.ppkn install_printer Top_printers.ppmind +install_printer Top_printers.ppind install_printer Top_printers.ppsp install_printer Top_printers.ppqualid install_printer Top_printers.ppclindex +install_printer Top_printers.ppscheme install_printer Top_printers.ppwf_paths install_printer Top_printers.ppevar install_printer Top_printers.ppconstr +install_printer Top_printers.ppsconstr install_printer Top_printers.ppeconstr +install_printer Top_printers.ppconstr_expr install_printer Top_printers.ppglob_constr install_printer Top_printers.pppattern install_printer Top_printers.ppfconstr @@ -30,21 +36,32 @@ install_printer Top_printers.ppevarsubst install_printer Top_printers.ppunbound_ltac_var_map install_printer Top_printers.ppclosure install_printer Top_printers.ppclosedglobconstr +install_printer Top_printers.ppclosedglobconstridmap +install_printer Top_printers.ppglobal +install_printer Top_printers.ppconst +install_printer Top_printers.ppvar install_printer Top_printers.ppj install_printer Top_printers.ppsubst install_printer Top_printers.ppdelta +install_printer Top_printers.pp_idpred +install_printer Top_printers.pp_cpred install_printer Top_printers.pp_transparent_state install_printer Top_printers.pp_stack_t install_printer Top_printers.pp_cst_stack_t +install_printer Top_printers.pp_state_t install_printer Top_printers.ppmetas install_printer Top_printers.ppevm install_printer Top_printers.ppexistentialset install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppclenv install_printer Top_printers.ppgoalgoal install_printer Top_printers.ppgoal install_printer Top_printers.pphintdb install_printer Top_printers.ppproofview +install_printer Top_printers.ppopenconstr +install_printer Top_printers.pproof install_printer Top_printers.ppuni +install_printer Top_printers.ppuni_level install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context @@ -54,6 +71,8 @@ install_printer Top_printers.ppuniverse_opt_subst install_printer Top_printers.ppuniverse_level_subst install_printer Top_printers.ppevar_universe_context install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuniverseconstraints +install_printer Top_printers.ppuniverse_context_future install_printer Top_printers.ppcumulativity_info install_printer Top_printers.ppabstract_cumulativity_info install_printer Top_printers.ppuniverses @@ -62,6 +81,8 @@ install_printer Top_printers.ppenv install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc +install_printer Top_printers.pp_argument_type +install_printer Top_printers.pp_generic_argument install_printer Top_printers.ppgenarginfo install_printer Top_printers.ppgenargargt install_printer Top_printers.ppist -- cgit v1.2.3