Module `Top_printers`Source

Printers for the OCaml toplevel.

Sourceval pp : Pp.t -> unit

Sourceval pP : Pp.t -> unit

Sourceval ppexninfo : Exninfo.info -> unit

Sourceval pp_as_format : Pp.t -> unit

Sourceval ppfuture : 'a Future.computation -> unit

Sourceval ppid : Names.Id.t -> unit

Sourceval ppmbid : Names.MBId.t -> unit

Sourceval ppdir : Names.DirPath.t -> unit

Sourceval ppmp : Names.ModPath.t -> unit

Sourceval ppcon : Names.Constant.t -> unit

Sourceval ppproj : Names.Projection.t -> unit

Sourceval ppprojrepr : Names.Projection.Repr.t -> unit

Sourceval ppkn : Names.KerName.t -> unit

Sourceval ppmind : Names.MutInd.t -> unit

Sourceval ppind : Names.inductive -> unit

Sourceval ppseff : Safe_typing.private_constants -> unit

Sourceval ppuint63 : Uint63.t -> unit

Sourceval ppsp : Libnames.full_path -> unit

Sourceval ppqualid : Libnames.qualid -> unit

Sourceval ppscheme : 'a Ind_tables.scheme_kind -> unit

Sourceval pprecarg : Declarations.recarg -> unit

Sourceval ppwf_paths : Declarations.recarg Rtree.t -> unit

Sourceval pr_evar : Evar.t -> Pp.t

Sourceval ppevar : Evar.t -> unit

Sourceval ppconstr : Constr.t -> unit

Sourceval ppconstr_univ : Constr.t -> unit

Sourceval pp_constr_parray : Constr.t Parray.t -> unit

Sourceval pp_fconstr_parray : CClosure.fconstr Parray.t -> unit

Sourceval pptype : Constr.types -> unit

Sourceval ppeconstr : EConstr.constr -> unit

Sourceval ppconstr_expr : Constrexpr.constr_expr -> unit

Sourceval ppglob_constr : 'a Glob_term.glob_constr_g -> unit

Sourceval pppattern : Pattern.constr_pattern -> unit

Sourceval ppfconstr : CClosure.fconstr -> unit

Sourceval pphconstr : HConstr.t -> unit

Sourceval pplift : Esubst.lift -> unit

Sourceval ppfsubst : CClosure.fconstr Esubst.subs -> unit

Sourceval ppnumtokunsigned : NumTok.Unsigned.t -> unit

Sourceval ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit

Sourceval ppintset : Int.Set.t -> unit

Sourceval ppidset : Names.Id.Set.t -> unit

Sourceval pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t

Sourceval ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit

Sourceval pridmapgen : 'a Names.Id.Map.t -> Pp.t

Sourceval ppidmapgen : 'a Names.Id.Map.t -> unit

Sourceval printmapgen : 'a Int.Map.t -> Pp.t

Sourceval ppintmapgen : 'a Int.Map.t -> unit

Sourceval ppmpmapgen : 'a Names.ModPath.Map.t -> unit

Sourceval ppdpmapgen : 'a Names.DirPath.Map.t -> unit

Sourceval ppconmapenvgen : 'a Names.Cmap_env.t -> unit

Sourceval ppmindmapenvgen : 'a Names.Mindmap_env.t -> unit

Sourceval prididmap : Names.Id.t Names.Id.Map.t -> Pp.t

Sourceval ppididmap : Names.Id.t Names.Id.Map.t -> unit

Source

val prconstrunderbindersidmap : 
  (Names.Id.t list * EConstr.constr) Names.Id.Map.t ->
  Pp.t

Source

val ppconstrunderbindersidmap : 
  (Names.Id.t list * EConstr.constr) Names.Id.Map.t ->
  unit

Source

val ppevarsubst : 
  (Constr.t * Constr.t option * Names.Id.Map.key) list Names.Id.Map.t ->
  unit

Sourceval ppunbound_ltac_var_map : 'a Genarg.generic_argument Names.Id.Map.t -> unit

Sourceval ppgenlam : _ Genlambda.lambda -> unit

Sourceval pr_closure : Ltac_pretype.closure -> Pp.t

Source

val pr_closed_glob_constr_idmap : 
  Ltac_pretype.closed_glob_constr Names.Id.Map.t ->
  Pp.t

Sourceval pr_closed_glob_constr : Ltac_pretype.closed_glob_constr -> Pp.t

Sourceval ppclosure : Ltac_pretype.closure -> unit

Sourceval ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit

Source

val ppclosedglobconstridmap : 
  Ltac_pretype.closed_glob_constr Names.Id.Map.t ->
  unit

Sourceval ppglobal : Names.GlobRef.t -> unit

Source

val ppconst : 
  (Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment) ->
  unit

Sourceval ppvar : (Names.Id.t * Constr.constr) -> unit

Sourceval genppj : ('a -> Pp.t * Pp.t) -> 'a -> Pp.t

Sourceval ppj : EConstr.unsafe_judgment -> unit

Sourceval ppsubst : Mod_subst.substitution -> unit

Sourceval ppdelta : Mod_subst.delta_resolver -> unit

Sourceval pp_idpred : Names.Id.Pred.t -> unit

Sourceval pp_cpred : Names.Cpred.t -> unit

Sourceval pp_transparent_state : TransparentState.t -> unit

Sourceval pp_estack_t : Reductionops.Stack.t -> unit

Sourceval pp_state_t : Reductionops.state -> unit

Sourceval ppmetas : Unification.Metaset.t -> unit

Sourceval ppmetamap : Unification.Meta.t -> unit

Sourceval ppevm : Evd.evar_map -> unit

Sourceval ppevmall : Evd.evar_map -> unit

Sourceval pr_existentialset : Evar.Set.t -> Pp.t

Sourceval ppexistentialset : Evar.Set.t -> unit

Sourceval ppexistentialfilter : Evd.Filter.t -> unit

Sourceval ppclenv : Clenv.clausenv -> unit

Sourceval ppgoal : Proofview.Goal.t -> unit

Sourceval ppgoal_with_state : Proofview_monad.goal_with_state -> unit

Sourceval pphintdb : Hints.Hint_db.t -> unit

Sourceval ppproofview : Proofview.proofview -> unit

Sourceval pproof : Proof.t -> unit

Sourceval ppuni : Univ.Universe.t -> unit

Sourceval ppuni_level : Univ.Level.t -> unit

Sourceval ppqvar : Sorts.QVar.t -> unit

Sourceval ppesorts : EConstr.ESorts.t -> unit

Sourceval pperelevance : EConstr.ERelevance.t -> unit

Sourceval prlev : Univ.Level.t -> Pp.t

Sourceval ppqvarset : Sorts.QVar.Set.t -> unit

Sourceval ppqset : Sorts.Quality.Set.t -> unit

Sourceval ppuniverse_set : Univ.Level.Set.t -> unit

Sourceval ppuniverse_instance : UVars.Instance.t -> unit

Sourceval ppuniverse_einstance : EConstr.EInstance.t -> unit

Sourceval ppuniverse_context : UVars.UContext.t -> unit

Sourceval ppaucontext : UVars.AbstractContext.t -> unit

Sourceval ppuniverse_subst : UnivSubst.universe_subst -> unit

Sourceval ppuniverse_opt_subst : UState.universe_opt_subst -> unit

Sourceval pppoly_flags : PolyFlags.t -> unit

Sourceval ppqvar_subst : Sorts.Quality.t Sorts.QVar.Map.t -> unit

Sourceval ppuniverse_level_subst : UVars.universe_level_subst -> unit

Sourceval ppustate : UState.t -> unit

Sourceval ppconstraints : Univ.UnivConstraints.t -> unit

Sourceval ppqconstraints : Sorts.ElimConstraints.t -> unit

Sourceval ppuniverseconstraints : UnivProblem.Set.t -> unit

Sourceval ppuniverse_context_future : UVars.UContext.t Future.computation -> unit

Sourceval ppuniverses : UGraph.t -> unit

Sourceval ppqualities : QGraph.t -> unit

Sourceval ppelim_constraints : Sorts.ElimConstraints.t -> unit

Source

val pp_partialfsubst : 
  (CClosure.fconstr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t ->
  unit

Source

val pp_partialsubst : 
  (EConstr.constr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t ->
  unit

Sourceval ppnamedcontextval : Environ.named_context_val -> unit

Sourceval ppenv : Environ.env -> unit

Sourceval ppglobenv : GlobEnv.t -> unit

Sourceval ppenvwithcst : Environ.env -> unit

Sourceval pptac : Ltac_plugin.Tacexpr.glob_tactic_expr -> unit

Sourceval ppobj : Libobject.obj -> unit

Sourceval cast_kind_display : Constr.cast_kind -> string

Sourceval constr_display : Constr.constr -> unit

Sourceval econstr_display : EConstr.constr -> unit

Sourceval print_pure_constr : Constr.types -> unit

Sourceval print_pure_econstr : EConstr.types -> unit

Sourceval pploc : Loc.t -> unit

Sourceval pp_argument_type : Genarg.argument_type -> unit

Sourceval pp_generic_argument : 'a Genarg.generic_argument -> unit

Sourceval prgenarginfo : Geninterp.Val.t -> Pp.t

Sourceval ppgenarginfo : Geninterp.Val.t -> unit

Sourceval ppgenargargt : ('a, 'b, 'c) Genarg.ArgT.tag -> unit

Sourceval ppist : Ltac_plugin.Tacinterp.interp_sign -> unit

Source

val raw_string_of_ref : 
  ?loc:Loc.t ->
  Names.Id.Set.t ->
  Names.GlobRef.t ->
  Libnames.qualid

Source

val short_string_of_ref : 
  ?loc:Loc.t ->
  Names.Id.Set.t ->
  Names.GlobRef.t ->
  Libnames.qualid

package rocq-runtime

Module Top_printersSource

Module `Top_printers`Source