package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
val allocc : Ssrast.ssrocc
val hyp_id : Ssrast.ssrhyp -> Names.Id.t
val hyps_ids : Ssrast.ssrhyps -> Names.Id.t list
val check_hyp_exists : ('a, 'b) Context.Named.pt -> Ssrast.ssrhyp -> unit
val test_hyp_exists : ('a, 'b) Context.Named.pt -> Ssrast.ssrhyp -> bool
val check_hyps_uniq : Names.Id.t list -> Ssrast.ssrhyps -> unit
val not_section_id : Names.Id.t -> bool
val hyp_err : ?loc:Loc.t -> string -> Names.Id.t -> 'a
val hoik : (Ssrast.ssrhyp -> 'a) -> Ssrast.ssrhyp_or_id -> 'a
val mk_hint : 'a -> 'a Ssrast.ssrhint
val mk_orhint : 'a -> bool * 'a
val nullhint : bool * 'a list
val nohint : 'a Ssrast.ssrhint
val errorstrm : Pp.t -> 'a
val anomaly : string -> 'a
val array_app_tl : 'a array -> 'a list -> 'a list
val array_list_of_tl : 'a array -> 'a list
val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
val option_assert_get : 'a option -> Pp.t -> 'a
val mkRHole : Glob_term.glob_constr
val mkRHoles : int -> Glob_term.glob_constr list
val isRHoles : Glob_term.glob_constr list -> bool
val mkRltacVar : Names.Id.t -> Glob_term.glob_constr
val mkRType : Glob_term.glob_constr
val mkRProp : Glob_term.glob_constr
val mkRnat : int -> Glob_term.glob_constr
val mkCHole : Loc.t option -> Constrexpr.constr_expr
val mkCHoles : ?loc:Loc.t -> int -> Constrexpr.constr_expr list
val mkCVar : ?loc:Loc.t -> Names.Id.t -> Constrexpr.constr_expr
val mkCType : Loc.t option -> Constrexpr.constr_expr
val mkCProp : Loc.t option -> Constrexpr.constr_expr
val isCHoles : Constrexpr.constr_expr list -> bool
val isCxHoles : (Constrexpr.constr_expr * 'a option) list -> bool
val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool
val mk_ast_closure_term : [ `None | `Parens | `DoubleParens | `At ] -> Constrexpr.constr_expr -> Ssrast.ast_closure_term
val ssrterm_of_ast_closure_term : Ssrast.ast_closure_term -> Ssrast.ssrterm
val is_internal_name : string -> bool
val add_internal_name : (string -> bool) -> unit
val mk_internal_id : string -> Names.Id.t
val mk_tagged_id : string -> int -> Names.Id.t
val mk_evar_name : int -> Names.Name.t
val ssr_anon_hyp : string
val abs_evars : Environ.env -> Evd.evar_map -> ?rigid:Evar.t list -> (Evd.evar_map * EConstr.t) -> EConstr.t * Evar.t list * UState.t
val abs_cterm : Environ.env -> Evd.evar_map -> int -> EConstr.t -> EConstr.t
val constr_name : Evd.evar_map -> EConstr.t -> Names.Name.t
val mkSsrRef : string -> Names.GlobRef.t
val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
val mkSsrConst : Environ.env -> Evd.evar_map -> string -> Evd.evar_map * EConstr.t
val is_discharged_id : Names.Id.t -> bool
val mk_discharged_id : Names.Id.t -> Names.Id.t
val is_tagged : string -> string -> bool
val has_discharged_tag : string -> bool
val ssrqid : string -> Libnames.qualid
val mk_anon_id : string -> Names.Id.t list -> Names.Id.t
val nbargs_open_constr : Environ.env -> (Evd.evar_map * EConstr.t) -> int
val pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int
val convert_concl_no_check : EConstr.t -> unit Proofview.tactic
val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic
val red_product_skip_id : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t
val ssrautoprop_tac : unit Proofview.tactic ref
val mkEtaApp : EConstr.t -> int -> int -> EConstr.t
val discharge_hyp : (Names.Id.t * (Names.Id.t * string)) -> unit Proofview.tactic
val view_error : string -> Ssrast.ssrterm -> 'a Proofview.tactic
val top_id : Names.Id.t
val abs_ssrterm : ?resolve_typeclasses:bool -> Ssrast.ist -> Environ.env -> Evd.evar_map -> Ssrast.ssrterm -> Evd.evar_map * EConstr.t * int
val ssr_n_tac : string -> int -> unit Proofview.tactic
val donetac : int -> unit Proofview.tactic
val applyn : with_evars:bool -> ?beta:bool -> ?with_shelve:bool -> ?first_goes_last:bool -> int -> EConstr.t -> unit Proofview.tactic
exception NotEnoughProducts
val saturate : ?beta:bool -> ?bi_types:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> ?ty:EConstr.types -> int -> EConstr.constr * EConstr.types * (int * EConstr.constr * EConstr.types) list * Evd.evar_map
val refine_with : ?first_goes_last:bool -> ?beta:bool -> ?with_evars:bool -> (Evd.evar_map * EConstr.t) -> unit Proofview.tactic
val resolve_typeclasses : Environ.env -> Evd.evar_map -> where:EConstr.t -> fail:bool -> Evd.evar_map
val rewritetac : ?under:bool -> Ssrast.ssrdir -> EConstr.t -> unit Proofview.tactic
type name_hint = (int * EConstr.types array) option ref

Basic tactics

val introid : ?orig:Names.Name.t ref -> Names.Id.t -> unit Proofview.tactic
val intro_anon : unit Proofview.tactic
val genclrtac : EConstr.constr -> EConstr.constr list -> Ssrast.ssrhyp list -> unit Proofview.tactic
val cleartac : Ssrast.ssrhyps -> unit Proofview.tactic
val tclMULT : (int * Ssrast.ssrmmod) -> unit Proofview.tactic -> unit Proofview.tactic
val unprotecttac : unit Proofview.tactic
val is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool
val abs_wgen : Environ.env -> Evd.evar_map -> bool -> (Names.Id.t -> Names.Id.t) -> ('a * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option) -> (EConstr.t list * EConstr.t) -> Evd.evar_map * EConstr.t list * EConstr.t
val clr_of_wgen : (Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * 'a) * 'b option) option) -> unit Proofview.tactic list -> unit Proofview.tactic list
val unfold : EConstr.t list -> unit Proofview.tactic
val tclINTERP_AST_CLOSURE_TERM_AS_CONSTR : Ssrast.ast_closure_term -> EConstr.t list Proofview.tactic
val tclINTRO_ID : Names.Id.t -> unit Proofview.tactic
val tclINTRO_ANON : ?seed:string -> unit -> unit Proofview.tactic
type intro_id =
  1. | Anon
  2. | Id of Names.Id.t
  3. | Seed of string
val tclINTRO : id:intro_id -> conclusion: (orig_name:Names.Name.t -> new_name:Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val tclRENAME_HD_PROD : Names.Name.t -> unit Proofview.tactic
val tcl0G : default:'a -> 'a Proofview.tactic -> 'a Proofview.tactic
val tclFIRSTa : 'a Proofview.tactic list -> 'a Proofview.tactic
val tclFIRSTi : (int -> 'a Proofview.tactic) -> int -> 'a Proofview.tactic
val tacCONSTR_NAME : ?name:Names.Name.t -> EConstr.t -> Names.Name.t Proofview.tactic
val tacUNIFY : EConstr.t -> EConstr.t -> unit Proofview.tactic
val tacIS_INJECTION_CASE : ?ty:EConstr.types -> EConstr.t -> bool Proofview.tactic
val tclWITHTOP : (EConstr.t -> unit Proofview.tactic) -> unit Proofview.tactic

1 shot, hands-on the top of the stack, eg for => ->

val tacMK_SSR_CONST : string -> EConstr.t Proofview.tactic
module type StateType = sig ... end
module MakeState (S : StateType) : sig ... end
val is_ind_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
val is_construct_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
val is_const_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
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