Module `Ssreflect_plugin.Ssrcommon`Source

Sourceval allocc : Ssrast.ssrocc

Sourceval hyp_id : Ssrast.ssrhyp -> Names.Id.t

Sourceval hyps_ids : Ssrast.ssrhyps -> Names.Id.t list

Sourceval check_hyp_exists : ('a, 'b) Context.Named.pt -> Ssrast.ssrhyp -> unit

Sourceval test_hyp_exists : ('a, 'b) Context.Named.pt -> Ssrast.ssrhyp -> bool

Sourceval check_hyps_uniq : Names.Id.t list -> Ssrast.ssrhyps -> unit

Sourceval not_section_id : Names.Id.t -> bool

Sourceval hyp_err : ?loc:Loc.t -> string -> Names.Id.t -> 'a

Sourceval hoik : (Ssrast.ssrhyp -> 'a) -> Ssrast.ssrhyp_or_id -> 'a

Sourceval hoi_id : Ssrast.ssrhyp_or_id -> Names.Id.t

Sourceval mk_hint : 'a -> 'a Ssrast.ssrhint

Sourceval mk_orhint : 'a -> bool * 'a

Sourceval nullhint : bool * 'a list

Sourceval nohint : 'a Ssrast.ssrhint

Sourceval errorstrm : Pp.t -> 'a

Sourceval anomaly : string -> 'a

Sourceval array_app_tl : 'a array -> 'a list -> 'a list

Sourceval array_list_of_tl : 'a array -> 'a list

Sourceval array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b

Sourceval option_assert_get : 'a option -> Pp.t -> 'a

Source

type 'a tac_a =
  (Ssrast.goal * 'a) Ssrast.sigma ->
  (Ssrast.goal * 'a) list Ssrast.sigma

Sourcetype 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;

}

Sourceval new_ctx : unit -> tac_ctx

Source

val pull_ctxs : 
  ('a * tac_ctx) list Ssrast.sigma ->
  'a list Ssrast.sigma * tac_ctx list

Sourceval with_fresh_ctx : tac_ctx tac_a -> Tacmach.tactic

Sourceval pull_ctx : ('a * tac_ctx) Ssrast.sigma -> 'a Ssrast.sigma * tac_ctx

Sourceval push_ctx : tac_ctx -> 'a Ssrast.sigma -> ('a * tac_ctx) Ssrast.sigma

Source

val push_ctxs : 
  tac_ctx ->
  'a list Ssrast.sigma ->
  ('a * tac_ctx) list Ssrast.sigma

Sourceval tac_ctx : Tacmach.tactic -> tac_ctx tac_a

Source

val with_ctx : 
  (tac_ctx -> 'b * tac_ctx) ->
  ('a * tac_ctx) Ssrast.sigma ->
  'b * ('a * tac_ctx) Ssrast.sigma

Sourceval without_ctx : ('a Ssrast.sigma -> 'b) -> ('a * tac_ctx) Ssrast.sigma -> 'b

Sourceval tclTHENLIST_a : tac_ctx tac_a list -> tac_ctx tac_a

Source

val tclTHEN_i_max : 
  tac_ctx tac_a ->
  (int -> int -> tac_ctx tac_a) ->
  tac_ctx tac_a

Sourceval tclTHEN_a : tac_ctx tac_a -> tac_ctx tac_a -> tac_ctx tac_a

Sourceval tclTHENS_a : tac_ctx tac_a -> tac_ctx tac_a list -> tac_ctx tac_a

Source

val tac_on_all : 
  (Ssrast.goal * tac_ctx) list Ssrast.sigma ->
  tac_ctx tac_a ->
  (Ssrast.goal * tac_ctx) list Ssrast.sigma

Sourceval mkRHole : Glob_term.glob_constr

Sourceval mkRHoles : int -> Glob_term.glob_constr list

Sourceval isRHoles : Glob_term.glob_constr list -> bool

Source

val mkRApp : 
  Glob_term.glob_constr ->
  Glob_term.glob_constr list ->
  Glob_term.glob_constr

Sourceval mkRVar : Names.Id.t -> Glob_term.glob_constr

Sourceval mkRltacVar : Names.Id.t -> Glob_term.glob_constr

Source

val mkRCast : 
  Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Sourceval mkRType : Glob_term.glob_constr

Sourceval mkRProp : Glob_term.glob_constr

Source

val mkRArrow : 
  Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Sourceval mkRConstruct : Names.constructor -> Glob_term.glob_constr

Sourceval mkRInd : Names.inductive -> Glob_term.glob_constr

Source

val mkRLambda : 
  Names.Name.t ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Sourceval mkRnat : int -> Glob_term.glob_constr

Sourceval mkCHole : Loc.t option -> Constrexpr.constr_expr

Sourceval mkCHoles : ?loc:Loc.t -> int -> Constrexpr.constr_expr list

Sourceval mkCVar : ?loc:Loc.t -> Names.Id.t -> Constrexpr.constr_expr

Source

val mkCCast : 
  ?loc:Loc.t ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Sourceval mkCType : Loc.t option -> Constrexpr.constr_expr

Sourceval mkCProp : Loc.t option -> Constrexpr.constr_expr

Source

val mkCArrow : 
  ?loc:Loc.t ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Source

val mkCLambda : 
  ?loc:Loc.t ->
  Names.Name.t ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr ->
  Constrexpr.constr_expr

Sourceval isCHoles : Constrexpr.constr_expr list -> bool

Sourceval isCxHoles : (Constrexpr.constr_expr * 'a option) list -> bool

Source

val intern_term : 
  Ltac_plugin.Tacinterp.interp_sign ->
  Environ.env ->
  Ssrast.ssrterm ->
  Glob_term.glob_constr

Source

val pf_intern_term : 
  Ltac_plugin.Tacinterp.interp_sign ->
  Goal.goal Evd.sigma ->
  Ssrast.ssrterm ->
  Glob_term.glob_constr

Source

val interp_term : 
  Environ.env ->
  Evd.evar_map ->
  Ltac_plugin.Tacinterp.interp_sign ->
  Ssrast.ssrterm ->
  Evd.evar_map * EConstr.t

Source

val interp_wit : 
  ('a, 'b, 'c) Genarg.genarg_type ->
  Ssrast.ist ->
  Ssrast.goal Ssrast.sigma ->
  'b ->
  Evd.evar_map * 'c

Source

val interp_hyp : 
  Ssrast.ist ->
  Ssrast.goal Ssrast.sigma ->
  Ssrast.ssrhyp ->
  Evd.evar_map * Ssrast.ssrhyp

Source

val interp_hyps : 
  Ssrast.ist ->
  Ssrast.goal Ssrast.sigma ->
  Ssrast.ssrhyps ->
  Evd.evar_map * Ssrast.ssrhyps

Source

val interp_refine : 
  Ltac_plugin.Tacinterp.interp_sign ->
  Goal.goal Evd.sigma ->
  Glob_term.glob_constr ->
  Evd.evar_map * (Evd.evar_map * EConstr.constr)

Source

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)

Source

val pf_e_type_of : 
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  Goal.goal Evd.sigma * EConstr.types

Source

val splay_open_constr : 
  Environ.env ->
  (Evd.evar_map * EConstr.t) ->
  (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t

Sourceval isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool

Sourceval mk_term : Ssrast.ssrtermkind -> Constrexpr.constr_expr -> Ssrast.ssrterm

Sourceval mk_lterm : Constrexpr.constr_expr -> Ssrast.ssrterm

Source

val mk_ast_closure_term : 
  [ `None | `Parens | `DoubleParens | `At ] ->
  Constrexpr.constr_expr ->
  Ssrast.ast_closure_term

Source

val interp_ast_closure_term : 
  Geninterp.interp_sign ->
  Goal.goal Evd.sigma ->
  Ssrast.ast_closure_term ->
  Evd.evar_map * Ssrast.ast_closure_term

Source

val subst_ast_closure_term : 
  Mod_subst.substitution ->
  Ssrast.ast_closure_term ->
  Ssrast.ast_closure_term

Source

val glob_ast_closure_term : 
  Genintern.glob_sign ->
  Ssrast.ast_closure_term ->
  Ssrast.ast_closure_term

Sourceval ssrterm_of_ast_closure_term : Ssrast.ast_closure_term -> Ssrast.ssrterm

Source

val ssrdgens_of_parsed_dgens : 
  ((Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list list
   * Ssrast.ssrclear) ->
  Ssrast.ssrdgens

Sourceval is_internal_name : string -> bool

Sourceval add_internal_name : (string -> bool) -> unit

Sourceval mk_internal_id : string -> Names.Id.t

Sourceval mk_tagged_id : string -> int -> Names.Id.t

Sourceval mk_evar_name : int -> Names.Name.t

Sourceval ssr_anon_hyp : string

Sourceval type_id : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Id.t

Sourceval pf_type_id : Goal.goal Evd.sigma -> EConstr.types -> Names.Id.t

Source

val abs_evars : 
  Environ.env ->
  Evd.evar_map ->
  (Evd.evar_map * EConstr.t) ->
  int * EConstr.t * Evar.t list * UState.t

Source

val abs_evars2 : 
  Environ.env ->
  Evd.evar_map ->
  Evar.t list ->
  (Evd.evar_map * EConstr.t) ->
  int * EConstr.t * Evar.t list * UState.t

Sourceval abs_cterm : Environ.env -> Evd.evar_map -> int -> EConstr.t -> EConstr.t

Source

val pf_abs_evars : 
  Goal.goal Evd.sigma ->
  (Evd.evar_map * EConstr.t) ->
  int * EConstr.t * Evar.t list * UState.t

Source

val pf_abs_evars2 : 
  Goal.goal Evd.sigma ->
  Evar.t list ->
  (Evd.evar_map * EConstr.t) ->
  int * EConstr.t * Evar.t list * UState.t

Sourceval pf_abs_cterm : Goal.goal Evd.sigma -> int -> EConstr.t -> EConstr.t

Sourceval pf_merge_uc : UState.t -> 'a Evd.sigma -> 'a Evd.sigma

Sourceval pf_merge_uc_of : Evd.evar_map -> 'a Evd.sigma -> 'a Evd.sigma

Sourceval constr_name : Evd.evar_map -> EConstr.t -> Names.Name.t

Source

val pf_type_of : 
  Goal.goal Evd.sigma ->
  Constr.constr ->
  Goal.goal Evd.sigma * Constr.types

Source

val pfe_type_of : 
  Goal.goal Evd.sigma ->
  EConstr.t ->
  Goal.goal Evd.sigma * EConstr.types

Sourceval pfe_new_type : Goal.goal Evd.sigma -> Goal.goal Evd.sigma * EConstr.types

Source

val pfe_type_relevance_of : 
  Goal.goal Evd.sigma ->
  EConstr.t ->
  Goal.goal Evd.sigma * EConstr.types * Sorts.relevance

Source

val pf_abs_prod : 
  Names.Name.t ->
  Goal.goal Evd.sigma ->
  EConstr.t ->
  EConstr.t ->
  Goal.goal Evd.sigma * EConstr.types

Sourceval mkSsrRRef : string -> Glob_term.glob_constr * 'a option

Sourceval new_wild_id : tac_ctx -> Names.Id.t * tac_ctx

Source

val pf_fresh_global : 
  Names.GlobRef.t ->
  Goal.goal Evd.sigma ->
  Constr.constr * Goal.goal Evd.sigma

Sourceval is_discharged_id : Names.Id.t -> bool

Sourceval mk_discharged_id : Names.Id.t -> Names.Id.t

Sourceval is_tagged : string -> string -> bool

Sourceval has_discharged_tag : string -> bool

Sourceval ssrqid : string -> Libnames.qualid

Sourceval new_tmp_id : tac_ctx -> (Names.Id.t * Names.Name.t Stdlib.ref) * tac_ctx

Sourceval mk_anon_id : string -> Names.Id.t list -> Names.Id.t

Source

val abs_evars_pirrel : 
  Environ.env ->
  Evd.evar_map ->
  (Evd.evar_map * Constr.constr) ->
  int * Constr.constr

Source

val pf_abs_evars_pirrel : 
  Goal.goal Evd.sigma ->
  (Evd.evar_map * Constr.constr) ->
  int * Constr.constr

Sourceval nbargs_open_constr : Environ.env -> (Evd.evar_map * EConstr.t) -> int

Sourceval pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int

Source

val gen_tmp_ids : 
  ?ist:Geninterp.interp_sign ->
  (Goal.goal * tac_ctx) Evd.sigma ->
  (Goal.goal * tac_ctx) list Evd.sigma

Source

val ssrevaltac : 
  Ltac_plugin.Tacinterp.interp_sign ->
  Ltac_plugin.Tacinterp.Value.t ->
  unit Proofview.tactic

Sourceval convert_concl_no_check : EConstr.t -> unit Proofview.tactic

Sourceval convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic

Source

val red_safe : 
  Reductionops.reduction_function ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.t ->
  EConstr.t

Sourceval red_product_skip_id : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t

Sourceval ssrautoprop_tac : unit Proofview.tactic Stdlib.ref

Source

val mkProt : 
  EConstr.t ->
  EConstr.t ->
  Goal.goal Evd.sigma ->
  EConstr.t * Goal.goal Evd.sigma

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

Source

val mkRefl : 
  EConstr.t ->
  EConstr.t ->
  Goal.goal Evd.sigma ->
  EConstr.t * Goal.goal Evd.sigma

Source

val discharge_hyp : 
  (Names.Id.t * (Names.Id.t * string)) ->
  Goal.goal Evd.sigma ->
  Evar.t list Evd.sigma

Source

val clear_wilds_and_tmp_and_delayed_ids : 
  (Goal.goal * tac_ctx) Evd.sigma ->
  (Goal.goal * tac_ctx) list Evd.sigma

Sourceval view_error : string -> Ssrast.ssrterm -> 'a

Sourceval top_id : Names.Id.t

Source

val pf_abs_ssrterm : 
  ?resolve_typeclasses:bool ->
  Ssrast.ist ->
  Goal.goal Evd.sigma ->
  Ssrast.ssrterm ->
  Evd.evar_map * EConstr.t * UState.t * int

Source

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

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

Sourceval donetac : int -> unit Proofview.tactic

Source

val applyn : 
  with_evars:bool ->
  ?beta:bool ->
  ?with_shelve:bool ->
  ?first_goes_last:bool ->
  int ->
  EConstr.t ->
  unit Proofview.tactic

Sourceexception NotEnoughProducts

Source

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

Source

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

Source

val refine_with : 
  ?first_goes_last:bool ->
  ?beta:bool ->
  ?with_evars:bool ->
  (Evd.evar_map * EConstr.t) ->
  unit Proofview.tactic

Source

val pf_resolve_typeclasses : 
  where:EConstr.t ->
  fail:bool ->
  Goal.goal Evd.sigma ->
  Goal.goal Evd.sigma

Source

val resolve_typeclasses : 
  where:EConstr.t ->
  fail:bool ->
  Environ.env ->
  Evd.evar_map ->
  Evd.evar_map

Source

val rewritetac : 
  ?under:bool ->
  Ssrast.ssrdir ->
  EConstr.t ->
  unit Proofview.tactic

Sourcetype name_hint = (int * EConstr.types array) option Stdlib.ref

Source

val gentac : 
  (Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) ->
  unit Proofview.tactic

Source

val genstac : 
  (((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ)
    * Ssrmatching_plugin.Ssrmatching.cpattern)
     list
   * Ssrast.ssrhyp list) ->
  unit Proofview.tactic

Source

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

Source

val pfLIFT : 
  (Goal.goal Evd.sigma -> 'a * Goal.goal Evd.sigma) ->
  'a Proofview.tactic

Basic tactics

Source

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

Sourceval intro_anon : Ssrast.v82tac

Source

val interp_clr : 
  Evd.evar_map ->
  (Ssrast.ssrhyps option * (Ssrast.ssrtermkind * EConstr.t)) ->
  Ssrast.ssrhyps

Source

val genclrtac : 
  EConstr.constr ->
  EConstr.constr list ->
  Ssrast.ssrhyp list ->
  Tacmach.tactic

Sourceval old_cleartac : Ssrast.ssrhyps -> Ssrast.v82tac

Sourceval cleartac : Ssrast.ssrhyps -> unit Proofview.tactic

Source

val tclMULT : 
  (int * Ssrast.ssrmmod) ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Sourceval unprotecttac : unit Proofview.tactic

Sourceval is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool

Source

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

Source

val clr_of_wgen : 
  (Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * 'a) * 'b option) option) ->
  unit Proofview.tactic list ->
  unit Proofview.tactic list

Sourceval unfold : EConstr.t list -> unit Proofview.tactic

Source

val apply_type : 
  EConstr.types ->
  EConstr.t list ->
  Evar.t Evd.sigma ->
  Evar.t list Evd.sigma

Sourceval tacSIGMA : Goal.goal Evd.sigma Proofview.tactic

Source

val tclINTERP_AST_CLOSURE_TERM_AS_CONSTR : 
  Ssrast.ast_closure_term ->
  EConstr.t list Proofview.tactic

Source

val tacREDUCE_TO_QUANTIFIED_IND : 
  EConstr.types ->
  ((Names.inductive * EConstr.EInstance.t) * EConstr.types) Proofview.tactic

Sourceval tacTYPEOF : EConstr.t -> EConstr.types Proofview.tactic

Sourceval tclINTRO_ID : Names.Id.t -> unit Proofview.tactic

Sourceval tclINTRO_ANON : ?seed:string -> unit -> unit Proofview.tactic

Sourcetype intro_id =

| Anon
| Id of Names.Id.t
| Seed of string

Source

val tclINTRO : 
  id:intro_id ->
  conclusion:
    (orig_name:Names.Name.t -> new_name:Names.Id.t -> unit Proofview.tactic) ->
  unit Proofview.tactic

Sourceval tclRENAME_HD_PROD : Names.Name.t -> unit Proofview.tactic

Sourceval tcl0G : default:'a -> 'a Proofview.tactic -> 'a Proofview.tactic

Sourceval tclFIRSTa : 'a Proofview.tactic list -> 'a Proofview.tactic

Sourceval tclFIRSTi : (int -> 'a Proofview.tactic) -> int -> 'a Proofview.tactic

Source

val tacCONSTR_NAME : 
  ?name:Names.Name.t ->
  EConstr.t ->
  Names.Name.t Proofview.tactic

Source

val tacMKPROD : 
  EConstr.t ->
  ?name:Names.Name.t ->
  EConstr.types ->
  EConstr.types Proofview.tactic

Source

val tacINTERP_CPATTERN : 
  Ssrmatching_plugin.Ssrmatching.cpattern ->
  Ssrmatching_plugin.Ssrmatching.pattern Proofview.tactic

Sourceval tacUNIFY : EConstr.t -> EConstr.t -> unit Proofview.tactic

Source

val tacIS_INJECTION_CASE : 
  ?ty:EConstr.types ->
  EConstr.t ->
  bool Proofview.tactic

Sourceval tclWITHTOP : (EConstr.t -> unit Proofview.tactic) -> unit Proofview.tactic

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

Sourceval tacMK_SSR_CONST : string -> EConstr.t Proofview.tactic

Sourcemodule type StateType = sig ... end

Sourcemodule MakeState (S : StateType) : sig ... end

Sourceval is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool

Sourceval is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool

Sourceval is_const_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssreflect_plugin/Ssreflect_plugin/Ssrcommon/index.html

Module `Ssreflect_plugin.Ssrcommon`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssreflect_plugin/Ssreflect_plugin/Ssrcommon/index.html

Module Ssreflect_plugin.SsrcommonSource

Module `Ssreflect_plugin.Ssrcommon`Source