package rocq-runtime

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

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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 pphconstr : HConstr.t -> 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 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 pperelevance : EConstr.ERelevance.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