Ssrcommon (rocq-runtime.Ssreflect

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, 'r) Context.Named.pt -> Ssrast.ssrhyp -> unit

val test_hyp_exists : ('a, 'b, 'r) 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

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 interp_term : Environ.env -> Evd.evar_map -> Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrterm -> Evd.evar_map * EConstr.t

val interp_hyp : Ssrast.ist -> Environ.env -> Evd.evar_map -> Ssrast.ssrhyp -> Ssrast.ssrhyp

val interp_hyps : Ssrast.ist -> Environ.env -> Evd.evar_map -> Ssrast.ssrhyps -> Ssrast.ssrhyps

val interp_refine : Environ.env -> Evd.evar_map -> Ltac_plugin.Tacinterp.interp_sign -> concl:EConstr.constr -> Glob_term.glob_constr -> 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 * EConstr.t

val splay_open_constr : Environ.env -> (Evd.evar_map * EConstr.t) -> (Names.Name.t EConstr.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 -> Environ.env -> Evd.evar_map -> Ssrast.ast_closure_term -> 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 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 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 : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t -> Evd.evar_map * EConstr.t

val mkEtaApp : EConstr.t -> int -> int -> EConstr.t

val mkRefl : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t -> Evd.evar_map * 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 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)) -> Evd.evar_map * int * EConstr.t * EConstr.t

val ssr_n_tac : string -> int -> unit Proofview.tactic

val donetac : int -> 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 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 interp_gen : Environ.env -> Evd.evar_map -> concl:EConstr.t -> bool -> ((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern) -> Evd.evar_map * (EConstr.t * EConstr.t * Ssrast.ssrhyp list)

Basic tactics

val introid : ?orig:Names.Name.t Stdlib.ref -> Names.Id.t -> unit Proofview.tactic

val intro_anon : unit Proofview.tactic

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 -> 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 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 (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