Module Ssreflect_plugin.Ssrcommon

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 hoi_id : Ssrast.ssrhyp_or_id -> Names.Id.t
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 = {
tmp_ids : (Names.Id.t * Names.Name.t Stdlib.ref) list;
wild_ids : Names.Id.t list;
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 mkRApp : Glob_term.glob_constr -> Glob_term.glob_constr list -> Glob_term.glob_constr
val mkRVar : Names.Id.t -> Glob_term.glob_constr
val mkRltacVar : Names.Id.t -> Glob_term.glob_constr
val mkRCast : Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
val mkRType : Glob_term.glob_constr
val mkRProp : Glob_term.glob_constr
val mkRArrow : Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
val mkRConstruct : Names.constructor -> Glob_term.glob_constr
val mkRInd : Names.inductive -> Glob_term.glob_constr
val mkRLambda : Names.Name.t -> Glob_term.glob_constr -> Glob_term.glob_constr -> 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 mkCCast : ?⁠loc:Loc.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val mkCType : Loc.t option -> Constrexpr.constr_expr
val mkCProp : Loc.t option -> Constrexpr.constr_expr
val mkCArrow : ?⁠loc:Loc.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val mkCLambda : ?⁠loc:Loc.t -> Names.Name.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val isCHoles : Constrexpr.constr_expr list -> bool
val isCxHoles : (Constrexpr.constr_expr * 'a option) list -> bool
val intern_term : Ltac_plugin.Tacinterp.interp_sign -> Environ.env -> Ssrast.ssrterm -> Glob_term.glob_constr
val pf_intern_term : Ltac_plugin.Tacinterp.interp_sign -> Goal.goal Evd.sigma -> Ssrast.ssrterm -> Glob_term.glob_constr
val interp_term : Environ.env -> Evd.evar_map -> Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrterm -> Evd.evar_map * EConstr.t
val interp_wit : ('a, 'b, 'c) Genarg.genarg_type -> Ssrast.ist -> Ssrast.goal Ssrast.sigma -> 'b -> Evd.evar_map * 'c
val interp_hyp : Ssrast.ist -> Ssrast.goal Ssrast.sigma -> Ssrast.ssrhyp -> Evd.evar_map * Ssrast.ssrhyp
val interp_hyps : Ssrast.ist -> Ssrast.goal Ssrast.sigma -> Ssrast.ssrhyps -> Evd.evar_map * Ssrast.ssrhyps
val interp_refine : Ltac_plugin.Tacinterp.interp_sign -> Goal.goal Evd.sigma -> Glob_term.glob_constr -> Evd.evar_map * (Evd.evar_map * EConstr.constr)
val interp_open_constr : Environ.env -> Evd.evar_map -> Ltac_plugin.Tacinterp.interp_sign -> Genintern.glob_constr_and_expr -> Evd.evar_map * (Evd.evar_map * EConstr.t)
val pf_e_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
val splay_open_constr : Environ.env -> (Evd.evar_map * EConstr.t) -> (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool
val mk_term : Ssrast.ssrtermkind -> Constrexpr.constr_expr -> Ssrast.ssrterm
val mk_lterm : Constrexpr.constr_expr -> Ssrast.ssrterm
val mk_ast_closure_term : [ `None | `Parens | `DoubleParens | `At ] -> Constrexpr.constr_expr -> Ssrast.ast_closure_term
val interp_ast_closure_term : Geninterp.interp_sign -> Goal.goal Evd.sigma -> Ssrast.ast_closure_term -> Evd.evar_map * Ssrast.ast_closure_term
val subst_ast_closure_term : Mod_subst.substitution -> Ssrast.ast_closure_term -> Ssrast.ast_closure_term
val glob_ast_closure_term : Genintern.glob_sign -> Ssrast.ast_closure_term -> Ssrast.ast_closure_term
val ssrterm_of_ast_closure_term : Ssrast.ast_closure_term -> Ssrast.ssrterm
val ssrdgens_of_parsed_dgens : ((Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list list * Ssrast.ssrclear) -> Ssrast.ssrdgens
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 type_id : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Id.t
val pf_type_id : Goal.goal Evd.sigma -> EConstr.types -> Names.Id.t
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 pf_type_of : Goal.goal Evd.sigma -> Constr.constr -> Goal.goal Evd.sigma * Constr.types
val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types
val pfe_new_type : Goal.goal Evd.sigma -> Goal.goal Evd.sigma * EConstr.types
val pfe_type_relevance_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types * Sorts.relevance
val pf_abs_prod : Names.Name.t -> Goal.goal Evd.sigma -> EConstr.t -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types
val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
val pf_fresh_global : Names.GlobRef.t -> Goal.goal Evd.sigma -> Constr.constr * Goal.goal Evd.sigma
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 Stdlib.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 ssrevaltac : Ltac_plugin.Tacinterp.interp_sign -> Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic
val convert_concl_no_check : EConstr.t -> unit Proofview.tactic
val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic
val red_safe : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t
val red_product_skip_id : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t
val ssrautoprop_tac : unit Proofview.tactic Stdlib.ref
val mkProt : EConstr.t -> EConstr.t -> Goal.goal Evd.sigma -> EConstr.t * Goal.goal Evd.sigma
val mkEtaApp : EConstr.t -> int -> int -> EConstr.t
val mkRefl : EConstr.t -> EConstr.t -> Goal.goal Evd.sigma -> EConstr.t * Goal.goal Evd.sigma
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 pf_interp_ty : ?⁠resolve_typeclasses:bool -> Environ.env -> Evd.evar_map -> Ltac_plugin.Tacinterp.interp_sign -> (Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option)) -> int * EConstr.t * EConstr.t * UState.t
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 Stdlib.ref
val gentac : (Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) -> unit Proofview.tactic
val genstac : (((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern) list * Ssrast.ssrhyp list) -> unit Proofview.tactic
val pf_interp_gen : bool -> ((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern) -> Goal.goal Evd.sigma -> (EConstr.t * EConstr.t * Ssrast.ssrhyp list) * Goal.goal Evd.sigma
val pfLIFT : (Goal.goal Evd.sigma -> 'a * Goal.goal Evd.sigma) -> 'a Proofview.tactic
val introid : ?⁠orig:Names.Name.t Stdlib.ref -> Names.Id.t -> unit Proofview.tactic
val intro_anon : Ssrast.v82tac
val interp_clr : Evd.evar_map -> (Ssrast.ssrhyps option * (Ssrast.ssrtermkind * EConstr.t)) -> Ssrast.ssrhyps
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 tacSIGMA : Goal.goal Evd.sigma Proofview.tactic
val tclINTERP_AST_CLOSURE_TERM_AS_CONSTR : Ssrast.ast_closure_term -> EConstr.t list Proofview.tactic
val tacREDUCE_TO_QUANTIFIED_IND : EConstr.types -> ((Names.inductive * EConstr.EInstance.t) * EConstr.types) Proofview.tactic
val tacTYPEOF : EConstr.t -> EConstr.types Proofview.tactic
val tclINTRO_ID : Names.Id.t -> unit Proofview.tactic
val tclINTRO_ANON : ?⁠seed:string -> unit -> unit Proofview.tactic
type intro_id =
| Anon
| Id of Names.Id.t
| 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 tacMKPROD : EConstr.t -> ?⁠name:Names.Name.t -> EConstr.types -> EConstr.types Proofview.tactic
val tacINTERP_CPATTERN : Ssrmatching_plugin.Ssrmatching.cpattern -> Ssrmatching_plugin.Ssrmatching.pattern 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 : functor (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