package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Printers for the ocaml toplevel.

val pp : Pp.t -> unit
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 ppprojrepr : Names.Projection.Repr.t -> unit
val ppkn : Names.KerName.t -> unit
val ppmind : Names.MutInd.t -> unit
val ppind : Names.inductive -> unit
val ppuint63 : Uint63.t -> unit
val ppsp : Libnames.full_path -> unit
val ppqualid : Libnames.qualid -> unit
val ppscheme : 'a Ind_tables.scheme_kind -> unit
val prrecarg : Declarations.recarg -> Pp.t
val ppwf_paths : Declarations.recarg Rtree.t -> unit
val pr_evar : Evar.t -> Pp.t
val ppevar : Evar.t -> unit
val ppconstr : Constr.t -> unit
val ppconstr_univ : Constr.t -> unit
val pp_constr_parray : Constr.t Parray.t -> unit
val pp_fconstr_parray : CClosure.fconstr Parray.t -> unit
val pptype : Constr.types -> unit
val ppeconstr : EConstr.constr -> unit
val ppconstr_expr : Constrexpr.constr_expr -> unit
val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
val pppattern : Pattern.constr_pattern -> unit
val ppfconstr : CClosure.fconstr -> unit
val ppfsubst : CClosure.fconstr Esubst.subs -> unit
val ppnumtokunsigned : NumTok.Unsigned.t -> unit
val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit
val ppintset : Int.Set.t -> unit
val ppidset : Names.Id.Set.t -> unit
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 printmapgen : 'a Int.Map.t -> Pp.t
val ppintmapgen : 'a Int.Map.t -> unit
val ppmpmapgen : 'a Names.MPmap.t -> unit
val ppdpmapgen : 'a Names.DPmap.t -> unit
val ppconmapenvgen : 'a Names.Cmap_env.t -> unit
val ppmindmapenvgen : 'a Names.Mindmap_env.t -> unit
val prmodidmapgen : 'a Names.ModIdmap.t -> Pp.t
val ppmodidmapgen : 'a Names.ModIdmap.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
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 ppglobal : Names.GlobRef.t -> 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 : TransparentState.t -> unit
val pp_estack_t : Reductionops.Stack.t -> unit
val pp_state_t : Reductionops.state -> unit
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 ppgoal : Proofview.Goal.t -> 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 ppqvar : Sorts.QVar.t -> unit
val ppesorts : EConstr.ESorts.t -> unit
val prlev : Univ.Level.t -> Pp.t
val ppuniverse_set : Univ.Level.Set.t -> unit
val ppuniverse_instance : Univ.Instance.t -> unit
val ppuniverse_context : Univ.UContext.t -> unit
val ppaucontext : Univ.AbstractContext.t -> unit
val ppuniverse_context_set : Univ.ContextSet.t -> unit
val ppuniverse_subst : UnivSubst.universe_subst -> unit
val ppuniverse_opt_subst : UState.universe_opt_subst -> unit
val ppuniverse_level_subst : Univ.universe_level_subst -> unit
val ppevar_universe_context : UState.t -> unit
val ppconstraints : Univ.Constraints.t -> unit
val ppuniverseconstraints : UnivProblem.Set.t -> unit
val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
val ppuniverses : UGraph.t -> unit
val ppnamedcontextval : Environ.named_context_val -> unit
val ppenv : Environ.env -> unit
val ppglobenv : GlobEnv.t -> unit
val ppenvwithcst : Environ.env -> unit
val ppobj : Libobject.obj -> unit
val cast_kind_display : Constr.cast_kind -> string
val constr_display : Constr.constr -> unit
val econstr_display : EConstr.constr -> unit
val print_pure_constr : Constr.types -> unit
val print_pure_econstr : EConstr.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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct