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.ml | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'pretyping/locusops.ml')

diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 3bbd8af443..5484c80950 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -80,3 +80,24 @@ let concrete_clause_of enum_hyps cl =
   if cl.concl_occs = NoOccurrences then hyps
   else
     OnConcl cl.concl_occs :: hyps
+
+(** Miscellaneous functions *)
+
+let out_arg = function
+  | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable")
+  | Misctypes.ArgArg x -> x
+
+let occurrences_of_hyp id cls =
+  let rec hyp_occ = function
+      [] -> NoOccurrences, InHyp
+    | ((occs,id'),hl)::_ when Names.Id.equal id id' ->
+        occurrences_map (List.map out_arg) occs, hl
+    | _::l -> hyp_occ l in
+  match cls.onhyps with
+      None -> AllOccurrences,InHyp
+    | Some l -> hyp_occ l
+
+let occurrences_of_goal cls =
+  occurrences_map (List.map out_arg) cls.concl_occs
+
+let in_every_hyp cls = Option.is_empty cls.onhyps
-- 
cgit v1.2.3