diff options
Diffstat (limited to 'pretyping/locusops.mli')
| -rw-r--r-- | pretyping/locusops.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index a086a6f58f..73d13c0bc0 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -35,3 +35,10 @@ val is_nowhere : 'a clause_expr -> bool val simple_clause_of : (unit -> Id.t list) -> clause -> simple_clause val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause + +(** Miscellaneous functions *) + +val occurrences_of_hyp : Id.t -> Id.t clause_expr -> + occurrences * hyp_location_flag +val occurrences_of_goal : 'a clause_expr -> occurrences +val in_every_hyp : 'a clause_expr -> bool |