Module Locus

type 'a or_var =
| ArgArg of 'a
| ArgVar of Names.lident
Occurrences
type 'a occurrences_gen =
| AllOccurrences
| AtLeastOneOccurrence
| AllOccurrencesBut of 'a list

non-empty

| NoOccurrences
| OnlyOccurrences of 'a list

non-empty

type occurrences_expr = int or_var occurrences_gen
type 'a with_occurrences = occurrences_expr * 'a
type occurrences = int occurrences_gen
Locations

Selecting the occurrences in body (if any), in type, or in both

type hyp_location_flag =
| InHyp
| InHypTypeOnly
| InHypValueOnly
Abstract clauses expressions

A clause_expr (and its instance clause) denotes occurrences and hypotheses in a goal in an abstract way; in particular, it can refer to the set of all hypotheses independently of the effective contents of the current goal

Concerning the field onhyps:

  • None means *on every hypothesis*
  • Some l means on hypothesis belonging to l
type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
type 'id clause_expr = {
onhyps : 'id hyp_location_expr list option;
concl_occs : occurrences_expr;
}
type clause = Names.Id.t clause_expr
Concrete view of occurrence clauses
type clause_atom =
| OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag
| OnConcl of occurrences_expr
type concrete_clause = clause_atom list
A weaker form of clause with no mention of occurrences
type hyp_location = Names.Id.t * hyp_location_flag
type goal_location = hyp_location option
Simple clauses, without occurrences nor location
type simple_clause = Names.Id.t option list
A notion of occurrences allowing to express "all occurrences convertible to the first which matches"
type 'a or_like_first =
| AtOccs of 'a
| LikeFirst