Module `Glob_ops`Source

Source

val map_glob_sort_gen : 
  ('a -> 'b) ->
  'a Glob_term.glob_sort_gen ->
  'b Glob_term.glob_sort_gen

Equalities

Source

val glob_sort_gen_eq : 
  ('a -> 'a -> bool) ->
  'a Glob_term.glob_sort_gen ->
  'a Glob_term.glob_sort_gen ->
  bool

Sourceval glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool

Sourceval glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool

Source

val cases_pattern_eq : 
  'a Glob_term.cases_pattern_g ->
  'a Glob_term.cases_pattern_g ->
  bool

Sourceexception ComplexSort

Expect a Prop/SProp/Set/Type universe; raise ComplexSort if contains a max, an increment, or a flexible universe

Sourceval glob_sort_family : Glob_term.glob_sort -> Sorts.family

Sourceval alias_of_pat : 'a Glob_term.cases_pattern_g -> Names.Name.t

Source

val set_pat_alias : 
  Names.Id.t ->
  'a Glob_term.cases_pattern_g ->
  'a Glob_term.cases_pattern_g

Source

val cast_type_eq : 
  ('a -> 'a -> bool) ->
  'a Glob_term.cast_type ->
  'a Glob_term.cast_type ->
  bool

Source

val glob_constr_eq : 
  'a Glob_term.glob_constr_g ->
  'a Glob_term.glob_constr_g ->
  bool

Mapping cast_type

Source

val map_cast_type : 
  ('a -> 'b) ->
  'a Glob_term.cast_type ->
  'b Glob_term.cast_type

Source

val smartmap_cast_type : 
  ('a -> 'a) ->
  'a Glob_term.cast_type ->
  'a Glob_term.cast_type

Operations on glob_constr

Sourceval cases_pattern_loc : 'a Glob_term.cases_pattern_g -> Loc.t option

Sourceval cases_predicate_names : 'a Glob_term.tomatch_tuples_g -> Names.Name.t list

Source

val mkGApp : 
  ?loc:Loc.t ->
  'a Glob_term.glob_constr_g ->
  'a Glob_term.glob_constr_g list ->
  'a Glob_term.glob_constr_g

Apply a list of arguments to a glob_constr

Source

val map_glob_constr : 
  (Glob_term.glob_constr -> Glob_term.glob_constr) ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Sourceval binding_kind_eq : Glob_term.binding_kind -> Glob_term.binding_kind -> bool

Equality on binding_kind

Source

val map_glob_constr_left_to_right : 
  (Glob_term.glob_constr -> Glob_term.glob_constr) ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

Ensure traversal from left to right

Sourceval warn_variable_collision : ?loc:Loc.t -> Names.Id.t -> unit

Source

val mk_glob_constr_eq : 
  (Glob_term.glob_constr -> Glob_term.glob_constr -> bool) ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr ->
  bool

Source

val fold_glob_constr : 
  ('a -> Glob_term.glob_constr -> 'a) ->
  'a ->
  Glob_term.glob_constr ->
  'a

Source

val fold_glob_constr_with_binders : 
  (Names.Id.t -> 'a -> 'a) ->
  ('a -> 'b -> Glob_term.glob_constr -> 'b) ->
  'a ->
  'b ->
  Glob_term.glob_constr ->
  'b

Source

val iter_glob_constr : 
  (Glob_term.glob_constr -> unit) ->
  Glob_term.glob_constr ->
  unit

Sourceval occur_glob_constr : Names.Id.t -> 'a Glob_term.glob_constr_g -> bool

Sourceval free_glob_vars : 'a Glob_term.glob_constr_g -> Names.Id.Set.t

Sourceval bound_glob_vars : Glob_term.glob_constr -> Names.Id.Set.t

Sourceval loc_of_glob_constr : 'a Glob_term.glob_constr_g -> Loc.t option

Sourceval glob_visible_short_qualid : 'a Glob_term.glob_constr_g -> Names.Id.Set.t

Sourceexception UnsoundRenaming

Sourceval rename_var : (Names.Id.t * Names.Id.t) list -> Names.Id.t -> Names.Id.t

Source

val rename_glob_vars : 
  (Names.Id.t * Names.Id.t) list ->
  'a Glob_term.glob_constr_g ->
  'a Glob_term.glob_constr_g

Source

val map_pattern_binders : 
  (Names.Name.t -> Names.Name.t) ->
  Glob_term.tomatch_tuples ->
  Glob_term.cases_clauses ->
  Glob_term.tomatch_tuples * Glob_term.cases_clauses

map_pattern_binders f m c applies f to all the binding names in a pattern-matching expression (Glob_term.glob_constr_r.GCases) represented here by its relevant components m and c. It is used to interpret Ltac-bound names both in pretyping and printing of terms.

Source

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

map_pattern f m c applies f to the return predicate and the right-hand side of a pattern-matching expression (Glob_term.glob_constr_r.GCases) represented here by its relevant components m and c.

Source

val cases_pattern_of_glob_constr : 
  Environ.env ->
  Names.Name.t ->
  'a Glob_term.glob_constr_g ->
  'a Glob_term.cases_pattern_g

Conversion from glob_constr to cases pattern, if possible

Evaluation is forced. Take the current alias as parameter,

raises Not_found
if translation is impossible

Source

val glob_constr_of_closed_cases_pattern : 
  Environ.env ->
  'a Glob_term.cases_pattern_g ->
  Names.Name.t * 'a Glob_term.glob_constr_g

Source

val glob_constr_of_cases_pattern : 
  Environ.env ->
  'a Glob_term.cases_pattern_g ->
  'a Glob_term.glob_constr_g

A canonical encoding of cases pattern into constr such that composed with cases_pattern_of_glob_constr Anonymous gives identity

Source

val add_patterns_for_params_remove_local_defs : 
  Environ.env ->
  Names.constructor ->
  'a Glob_term.cases_pattern_g list ->
  'a Glob_term.cases_pattern_g list

Sourceval empty_lvar : Ltac_pretype.ltac_var_map

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Glob_ops/index.html

Module `Glob_ops`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Glob_ops/index.html

Module Glob_opsSource

Module `Glob_ops`Source