LocusLocus : positions in hypotheses and goals
type occurrences_expr = int or_var occurrences_gentype 'a with_occurrences_expr = occurrences_expr * 'atype occurrences = int occurrences_gentype 'a with_occurrences = occurrences * 'aSelecting the occurrences in body (if any), in type, or in both
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 ltype 'a hyp_location_expr = 'a with_occurrences_expr * hyp_location_flagtype clause = Names.Id.t clause_exprclause_atom refers either to an hypothesis location (i.e. an hypothesis with occurrences and a position, in body if any, in type or in both) or to some occurrences of the conclusion
type clause_atom = | OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag |
| OnConcl of occurrences_expr |
A concrete_clause is an effective collection of occurrences in the hypotheses and the conclusion
type concrete_clause = clause_atom listA hyp_location is an hypothesis together with a location
type hyp_location = Names.Id.t * hyp_location_flagA goal_location is either an hypothesis (together with a location) or the conclusion (represented by None)
type goal_location = hyp_location optionA simple_clause is a set of hypotheses, possibly extended with the conclusion (conclusion is represented by None)
type simple_clause = Names.Id.t option list