package coq-core

  1. Overview
  2. Docs
package coq-core
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.

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