package coq

  1. Overview
  2. Docs
package coq
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
type 'a tac_a = (Ssrast.goal * 'a) Ssrast.sigma -> (Ssrast.goal * 'a) list Ssrast.sigma
type tac_ctx = {
  1. tmp_ids : (Names.Id.t * Names.Name.t ref) list;
  2. wild_ids : Names.Id.t list;
  3. delayed_clears : Names.Id.t list;
}
val new_ctx : unit -> tac_ctx
val pull_ctxs : ('a * tac_ctx) list Ssrast.sigma -> 'a list Ssrast.sigma * tac_ctx list
val with_fresh_ctx : tac_ctx tac_a -> Tacmach.tactic
val pull_ctx : ('a * tac_ctx) Ssrast.sigma -> 'a Ssrast.sigma * tac_ctx
val push_ctx : tac_ctx -> 'a Ssrast.sigma -> ('a * tac_ctx) Ssrast.sigma
val push_ctxs : tac_ctx -> 'a list Ssrast.sigma -> ('a * tac_ctx) list Ssrast.sigma
val tac_ctx : Tacmach.tactic -> tac_ctx tac_a
val with_ctx : (tac_ctx -> 'b * tac_ctx) -> ('a * tac_ctx) Ssrast.sigma -> 'b * ('a * tac_ctx) Ssrast.sigma
val without_ctx : ('a Ssrast.sigma -> 'b) -> ('a * tac_ctx) Ssrast.sigma -> 'b
val tclTHENLIST_a : tac_ctx tac_a list -> tac_ctx tac_a
val tclTHEN_i_max : tac_ctx tac_a -> (int -> int -> tac_ctx tac_a) -> tac_ctx tac_a
val tclTHEN_a : tac_ctx tac_a -> tac_ctx tac_a -> tac_ctx tac_a
val tclTHENS_a : tac_ctx tac_a -> tac_ctx tac_a list -> tac_ctx tac_a
val tac_on_all : (Ssrast.goal * tac_ctx) list Ssrast.sigma -> tac_ctx tac_a -> (Ssrast.goal * tac_ctx) list Ssrast.sigma
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 interp_wit : ('a, 'b, 'c) Genarg.genarg_type -> Ssrast.ist -> Ssrast.goal Ssrast.sigma -> 'b -> Evd.evar_map * 'c
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 -> (Evd.evar_map * EConstr.t) -> int * EConstr.t * Evar.t list * UState.t
val abs_evars2 : Environ.env -> Evd.evar_map -> Evar.t list -> (Evd.evar_map * EConstr.t) -> int * EConstr.t * Evar.t list * UState.t
val abs_cterm : Environ.env -> Evd.evar_map -> int -> EConstr.t -> EConstr.t
val pf_abs_evars : Goal.goal Evd.sigma -> (Evd.evar_map * EConstr.t) -> int * EConstr.t * Evar.t list * UState.t
val pf_abs_evars2 : Goal.goal Evd.sigma -> Evar.t list -> (Evd.evar_map * EConstr.t) -> int * EConstr.t * Evar.t list * UState.t
val pf_abs_cterm : Goal.goal Evd.sigma -> int -> EConstr.t -> EConstr.t
val pf_merge_uc : UState.t -> 'a Evd.sigma -> 'a Evd.sigma
val pf_merge_uc_of : Evd.evar_map -> 'a Evd.sigma -> 'a Evd.sigma
val constr_name : Evd.evar_map -> EConstr.t -> Names.Name.t
val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
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 new_tmp_id : tac_ctx -> (Names.Id.t * Names.Name.t ref) * tac_ctx
val mk_anon_id : string -> Names.Id.t list -> Names.Id.t
val abs_evars_pirrel : Environ.env -> Evd.evar_map -> (Evd.evar_map * Constr.constr) -> int * Constr.constr
val pf_abs_evars_pirrel : Goal.goal Evd.sigma -> (Evd.evar_map * Constr.constr) -> int * Constr.constr
val nbargs_open_constr : Environ.env -> (Evd.evar_map * EConstr.t) -> int
val pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int
val gen_tmp_ids : ?ist:Geninterp.interp_sign -> (Goal.goal * tac_ctx) Evd.sigma -> (Goal.goal * tac_ctx) list Evd.sigma
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)) -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma
val clear_wilds_and_tmp_and_delayed_ids : (Goal.goal * tac_ctx) Evd.sigma -> (Goal.goal * tac_ctx) list Evd.sigma
val view_error : string -> Ssrast.ssrterm -> 'a
val top_id : Names.Id.t
val pf_abs_ssrterm : ?resolve_typeclasses:bool -> Ssrast.ist -> Goal.goal Evd.sigma -> Ssrast.ssrterm -> Evd.evar_map * EConstr.t * UState.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 pf_saturate : ?beta:bool -> ?bi_types:bool -> Goal.goal Evd.sigma -> EConstr.constr -> ?ty:EConstr.types -> int -> EConstr.constr * EConstr.types * (int * EConstr.constr) list * Goal.goal Evd.sigma
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) 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 pf_resolve_typeclasses : where:EConstr.t -> fail:bool -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma
val resolve_typeclasses : where:EConstr.t -> fail:bool -> Environ.env -> Evd.evar_map -> 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 : Ssrast.v82tac
val genclrtac : EConstr.constr -> EConstr.constr list -> Ssrast.ssrhyp list -> Tacmach.tactic
val old_cleartac : Ssrast.ssrhyps -> Ssrast.v82tac
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 : bool -> (Names.Id.t -> Names.Id.t) -> ('a * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option) -> (Goal.goal Evd.sigma * EConstr.t list * EConstr.t) -> Goal.goal Evd.sigma * 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 apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac
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 : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
val is_const_ref : 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