From 56cb514b425360ca428be116e9ea1d5205edd06f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 29 Aug 2014 14:41:47 +0200 Subject: Moving function about locs in locusops. --- pretyping/locusops.mli | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'pretyping/locusops.mli') 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 -- cgit v1.2.3