Locusops (coq-core.Locusops)

val or_var_map : ( 'a -> 'b ) -> 'a Locus.or_var -> 'b Locus.or_var

Utilities on occurrences

val occurrences_map : 
  ( 'a list -> 'b list ) ->
  'a Locus.occurrences_gen ->
  'b Locus.occurrences_gen

type occurrences_count

A counter of occurrences associated to a list of occurrences

Three basic functions to initialize, count, and conclude a loop browsing over subterms

val initialize_occurrence_counter : Locus.occurrences -> occurrences_count

Initialize an occurrence_counter

val update_occurrence_counter : occurrences_count -> bool * occurrences_count

Increase the occurrence counter by one and tell if the current occurrence is selected

val check_used_occurrences : occurrences_count -> unit

Increase the occurrence counter and tell if the current occurrence is selected

Auxiliary functions about occurrence counters

val current_occurrence : occurrences_count -> int

Tell the value of the current occurrence

val occurrences_done : occurrences_count -> bool

Tell if there are no more occurrences to select and if the loop can be shortcut

val more_specific_occurrences : occurrences_count -> bool

Tell if there are no more occurrences to select (or unselect) and if an inner loop can be shortcut

val is_selected : int -> Locus.occurrences -> bool

val is_all_occurrences : 'a Locus.occurrences_gen -> bool

val error_invalid_occurrence : int list -> 'a

Usual clauses

val allHypsAndConcl : 'a Locus.clause_expr

val allHyps : 'a Locus.clause_expr

val onConcl : 'a Locus.clause_expr

val nowhere : 'a Locus.clause_expr

val onHyp : 'a -> 'a Locus.clause_expr

Tests

val is_nowhere : 'a Locus.clause_expr -> bool

Clause conversion functions, parametrized by a hyp enumeration function

val simple_clause_of : 
  ( unit -> Names.Id.t list ) ->
  Locus.clause ->
  Locus.simple_clause

val concrete_clause_of : 
  ( unit -> Names.Id.t list ) ->
  Locus.clause ->
  Locus.concrete_clause

Miscellaneous functions

val occurrences_of_hyp : 
  Names.Id.t ->
  Locus.clause ->
  Locus.occurrences * Locus.hyp_location_flag

val occurrences_of_goal : Locus.clause -> Locus.occurrences

val in_every_hyp : Locus.clause -> bool

val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool

val clause_with_generic_context_selection : 'a Locus.clause_expr -> bool