Glob_termops (coq-core.Funind_plugin.Glob

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

val pattern_to_term : Glob_term.cases_pattern -> Glob_term.glob_constr

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

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

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

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

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

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

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

val mkGHole : unit -> Glob_term.glob_constr

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

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

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

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

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

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

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

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

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

val are_unifiable : 
  Environ.env ->
  Glob_term.cases_pattern ->
  Glob_term.cases_pattern ->
  bool

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

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

val expand_as : Glob_term.glob_constr -> Glob_term.glob_constr

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