Moving function about locs in locusops.

1 files changed, 21 insertions, 0 deletions

diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 3bbd8af44..5484c8095 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