Module `Funind_plugin.Glob_termops`Source

Sourceval get_pattern_id : Glob_term.cases_pattern -> Names.Id.t list

Sourceval pattern_to_term : Glob_term.cases_pattern -> Glob_term.glob_constr

Sourceval mkGRef : Names.GlobRef.t -> Glob_term.glob_constr

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

val mkGApp : 
  (Glob_term.glob_constr * Glob_term.glob_constr list) ->
  Glob_term.glob_constr

Source

val mkGLambda : 
  (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) ->
  Glob_term.glob_constr

Source

val mkGProd : 
  (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) ->
  Glob_term.glob_constr

Source

val mkGLetIn : 
  (Names.Name.t
   * Glob_term.glob_constr
   * Glob_term.glob_constr option
   * Glob_term.glob_constr) ->
  Glob_term.glob_constr

Source

val mkGCases : 
  (Glob_term.glob_constr option
   * Glob_term.tomatch_tuples
   * Glob_term.cases_clauses) ->
  Glob_term.glob_constr

Sourceval mkGHole : unit -> Glob_term.glob_constr

Source

val glob_decompose_app : 
  Glob_term.glob_constr ->
  Glob_term.glob_constr * Glob_term.glob_constr list

Source

val glob_make_eq : 
  ?typ:Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Source

val glob_make_neq : 
  Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Source

val change_vars : 
  Names.Id.t Names.Id.Map.t ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Source

val alpha_pat : 
  Names.Id.Map.key list ->
  Glob_term.cases_pattern ->
  Glob_term.cases_pattern * Names.Id.Map.key list * Names.Id.t Names.Id.Map.t

Source

val alpha_rt : 
  Names.Id.t list ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Source

val alpha_br : 
  Names.Id.t list ->
  Glob_term.cases_clause ->
  Glob_term.cases_clause

Source

val replace_var_by_term : 
  Names.Id.t ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Sourceval is_free_in : Names.Id.t -> Glob_term.glob_constr -> bool

Sourceval are_unifiable : Glob_term.cases_pattern -> Glob_term.cases_pattern -> bool

Source

val eq_cases_pattern : 
  Glob_term.cases_pattern ->
  Glob_term.cases_pattern ->
  bool

Sourceval ids_of_pat : Glob_term.cases_pattern -> Names.Id.Set.t

Sourceval expand_as : Glob_term.glob_constr -> Glob_term.glob_constr

Source

val resolve_and_replace_implicits : 
  ?flags:Pretyping.inference_flags ->
  ?expected_type:Pretyping.typing_constraint ->
  Environ.env ->
  Evd.evar_map ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Install

Dune Dependency

Authors

Maintainers

Sources

doc/funind_plugin/Funind_plugin/Glob_termops/index.html

Module `Funind_plugin.Glob_termops`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/funind_plugin/Funind_plugin/Glob_termops/index.html

Module Funind_plugin.Glob_termopsSource

Module `Funind_plugin.Glob_termops`Source