diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-29 14:41:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-13 19:12:34 +0200 |
| commit | 56cb514b425360ca428be116e9ea1d5205edd06f (patch) | |
| tree | 2edec11d80f78c0caeae35913fa156768b9d3536 /pretyping/locusops.mli | |
| parent | c72eb85062edea223f5868c67ded99da7954d49a (diff) | |
Moving function about locs in locusops.
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 a086a6f58..73d13c0bc 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 |