package coq-core

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ssreflect_plugin.SsrcommonSource

Sourceval allocc : Ssrast.ssrocc
Sourceval hyps_ids : Ssrast.ssrhyps -> Names.Id.t list
Sourceval check_hyp_exists : ('a, 'b, 'r) Context.Named.pt -> Ssrast.ssrhyp -> unit
Sourceval test_hyp_exists : ('a, 'b, 'r) 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 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
Sourceval mkRHoles : int -> Glob_term.glob_constr list
Sourceval isRHoles : Glob_term.glob_constr list -> bool
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 mkCType : Loc.t option -> Constrexpr.constr_expr
Sourceval mkCProp : Loc.t option -> Constrexpr.constr_expr
Sourceval isCHoles : Constrexpr.constr_expr list -> bool
Sourceval isCxHoles : (Constrexpr.constr_expr * 'a option) list -> bool
Sourceval isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool
Sourceval mk_ast_closure_term : [ `None | `Parens | `DoubleParens | `At ] -> Constrexpr.constr_expr -> Ssrast.ast_closure_term
Sourceval ssrterm_of_ast_closure_term : Ssrast.ast_closure_term -> Ssrast.ssrterm
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 abs_evars : Environ.env -> Evd.evar_map -> ?rigid:Evar.t list -> (Evd.evar_map * EConstr.t) -> EConstr.t * Evar.t list * UState.t
Sourceval abs_cterm : Environ.env -> Evd.evar_map -> int -> EConstr.t -> EConstr.t
Sourceval constr_name : Evd.evar_map -> EConstr.t -> Names.Name.t
Sourceval mkSsrRef : string -> Names.GlobRef.t
Sourceval mkSsrRRef : string -> Glob_term.glob_constr * 'a option
Sourceval mkSsrConst : Environ.env -> Evd.evar_map -> string -> Evd.evar_map * EConstr.t
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 mk_anon_id : string -> Names.Id.t list -> Names.Id.t
Sourceval nbargs_open_constr : Environ.env -> (Evd.evar_map * EConstr.t) -> int
Sourceval pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int
Sourceval convert_concl_no_check : EConstr.t -> unit Proofview.tactic
Sourceval convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic
Sourceval red_product_skip_id : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t
Sourceval ssrautoprop_tac : unit Proofview.tactic Stdlib.ref
Sourceval mkEtaApp : EConstr.t -> int -> int -> EConstr.t
Sourceval discharge_hyp : (Names.Id.t * (Names.Id.t * string)) -> unit Proofview.tactic
Sourceval view_error : string -> Ssrast.ssrterm -> 'a Proofview.tactic
Sourceval top_id : Names.Id.t
Sourceval abs_ssrterm : ?resolve_typeclasses:bool -> Ssrast.ist -> Environ.env -> Evd.evar_map -> Ssrast.ssrterm -> Evd.evar_map * EConstr.t * int
Sourceval ssr_n_tac : string -> int -> unit Proofview.tactic
Sourceval donetac : int -> unit Proofview.tactic
Sourceexception NotEnoughProducts
Sourceval 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
Sourceval refine_with : ?first_goes_last:bool -> ?beta:bool -> ?with_evars:bool -> (Evd.evar_map * EConstr.t) -> unit Proofview.tactic
Sourceval resolve_typeclasses : Environ.env -> Evd.evar_map -> where:EConstr.t -> fail:bool -> Evd.evar_map
Sourceval rewritetac : ?under:bool -> Ssrast.ssrdir -> EConstr.t -> unit Proofview.tactic
Sourcetype name_hint = (int * EConstr.types array) option Stdlib.ref

Basic tactics

Sourceval introid : ?orig:Names.Name.t Stdlib.ref -> Names.Id.t -> unit Proofview.tactic
Sourceval intro_anon : unit Proofview.tactic
Sourceval genclrtac : EConstr.constr -> EConstr.constr list -> Ssrast.ssrhyp list -> unit Proofview.tactic
Sourceval cleartac : Ssrast.ssrhyps -> unit Proofview.tactic
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval tclINTERP_AST_CLOSURE_TERM_AS_CONSTR : Ssrast.ast_closure_term -> EConstr.t list Proofview.tactic
Sourceval tclINTRO_ID : Names.Id.t -> unit Proofview.tactic
Sourceval tclINTRO_ANON : ?seed:string -> unit -> unit Proofview.tactic
Sourcetype intro_id =
  1. | Anon
  2. | Id of Names.Id.t
  3. | Seed of string
Sourceval 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
Sourceval tacUNIFY : EConstr.t -> EConstr.t -> unit Proofview.tactic
Sourceval 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 : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
Sourceval is_construct_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
Sourceval is_const_ref : Environ.env -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
OCaml

Innovation. Community. Security.