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
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