package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type mutual
type individual
type 'a scheme_kind
type internal_flag =
  1. | UserAutomaticRequest
  2. | InternalTacticRequest
  3. | UserIndividualRequest
val declare_mutual_scheme_object : string -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind
val declare_individual_scheme_object : string -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind
val define_mutual_scheme : mutual scheme_kind -> internal_flag -> (int * Names.Id.t) list -> Names.MutInd.t -> Names.Constant.t array * Evd.side_effects
val check_scheme : 'a scheme_kind -> Names.inductive -> bool
val pr_scheme_kind : 'a scheme_kind -> Pp.t
OCaml

Innovation. Community. Security.