package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.dev/Top_printers/index.html

Module Top_printersSource

Printers for the OCaml toplevel.

Sourceval pp : Pp.t -> unit
Sourceval pP : Pp.t -> unit
Sourceval pp_as_format : Pp.t -> unit
Sourceval ppfuture : 'a Future.computation -> unit
Sourceval ppid : Names.Id.t -> unit
Sourceval pplab : Names.Label.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 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 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.MPmap.t -> unit
Sourceval ppdpmapgen : 'a Names.DPmap.t -> unit
Sourceval ppconmapenvgen : 'a Names.Cmap_env.t -> unit
Sourceval ppmindmapenvgen : 'a Names.Mindmap_env.t -> unit
Sourceval prmodidmapgen : 'a Names.ModIdmap.t -> Pp.t
Sourceval ppmodidmapgen : 'a Names.ModIdmap.t -> unit
Sourceval ppididmap : Names.Id.t Names.Id.Map.t -> unit
Sourceval prconstrunderbindersidmap : (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> Pp.t
Sourceval ppconstrunderbindersidmap : (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> unit
Sourceval 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 pr_closure : Ltac_pretype.closure -> Pp.t
Sourceval 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
Sourceval ppclosedglobconstridmap : Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit
Sourceval ppglobal : Names.GlobRef.t -> unit
Sourceval ppvar : (Names.Id.t * Constr.constr) -> unit
Sourceval genppj : ('a -> Pp.t * Pp.t) -> 'a -> Pp.t
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 ppopenconstr : Evd.open_constr -> 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 prlev : Univ.Level.t -> Pp.t
Sourceval ppqvarset : Sorts.QVar.Set.t -> unit
Sourceval ppuniverse_set : Univ.Level.Set.t -> unit
Sourceval ppuniverse_instance : UVars.Instance.t -> unit
Sourceval ppuniverse_context : UVars.UContext.t -> unit
Sourceval ppaucontext : UVars.AbstractContext.t -> unit
Sourceval ppuniverse_context_set : Univ.ContextSet.t -> unit
Sourceval ppuniverse_subst : UnivSubst.universe_subst -> unit
Sourceval ppuniverse_opt_subst : UState.universe_opt_subst -> unit
Sourceval ppqvar_subst : Sorts.Quality.t Sorts.QVar.Map.t -> unit
Sourceval ppuniverse_level_subst : Univ.universe_level_subst -> unit
Sourceval ppustate : UState.t -> unit
Sourceval ppconstraints : Univ.Constraints.t -> unit
Sourceval ppuniverseconstraints : UnivProblem.Set.t -> unit
Sourceval ppuniverse_context_future : UVars.UContext.t Future.computation -> unit
Sourceval ppuniverses : UGraph.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 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 : Geninterp.interp_sign -> unit
Sourceval raw_string_of_ref : ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
Sourceval short_string_of_ref : ?loc:Loc.t -> Names.Id.Set.t -> Names.GlobRef.t -> Libnames.qualid
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