diff options
Diffstat (limited to 'pretyping/locusops.ml')
| -rw-r--r-- | pretyping/locusops.ml | 21 |
1 files changed, 21 insertions, 0 deletions
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 |