package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val __coq_plugin_name : string
val pr_fun_ind_using : 'a -> 'b -> ('c -> 'd -> 'e -> Pp.t) -> ('f -> 'g -> 'e -> Pp.t) -> 'h -> ('e * 'e Tactypes.bindings) option -> Pp.t
val pr_fun_ind_using_typed : (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'b -> (Environ.env -> Evd.evar_map -> 'c * ('a * 'a Tactypes.bindings)) option -> Pp.t
val pr_intro_as_pat : 'a -> 'b -> 'c -> 'd option -> Pp.t
val pr_constr_comma_sequence : 'a -> 'b -> ('c -> 'd -> 'e -> Pp.t) -> 'f -> 'g -> 'e list -> Pp.t
val constr_comma_sequence' : Constrexpr.constr_expr list Pcoq.Entry.t
val pr_auto_using : 'a -> 'b -> ('c -> 'd -> 'e -> Pp.t) -> 'f -> 'g -> 'e list -> Pp.t
val auto_using' : Constrexpr.constr_expr list Pcoq.Entry.t
module Vernac = Pvernac.Vernac_
module Tactic = Ltac_plugin.Pltac
val function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Pcoq.Entry.t
val is_proof_termination_interactively_checked : ('a * Constrexpr.recursion_order_expr_r CAst.t option Vernacexpr.fix_expr_gen) list -> bool
val classify_as_Fixpoint : ('a * Vernacexpr.fixpoint_expr) list -> Vernacextend.vernac_classification
val is_interactive : ('a * Vernacexpr.fixpoint_expr) list -> bool
val pr_fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family) -> Pp.t
val wit_fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family, unit, unit) Genarg.genarg_type
val warning_error : Libnames.qualid list -> exn -> unit