diff options
Diffstat (limited to 'pretyping/locusops.ml')
| -rw-r--r-- | pretyping/locusops.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 9c6cf090a2..ffb29bb38c 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -71,12 +71,12 @@ let simple_clause_of enum_hyps cl = let hyps = match cl.onhyps with | None -> - List.map Option.make (enum_hyps ()) + List.map Option.make (enum_hyps ()) | Some l -> - List.map (fun ((occs,id),w) -> + List.map (fun ((occs,id),w) -> if not (is_all_occurrences occs) then error_occurrences (); - if w = InHypValueOnly then error_body_selection (); - Some id) l in + if w = InHypValueOnly then error_body_selection (); + Some id) l in if cl.concl_occs = NoOccurrences then hyps else if not (is_all_occurrences cl.concl_occs) then error_occurrences () @@ -88,10 +88,10 @@ let concrete_clause_of enum_hyps cl = let hyps = match cl.onhyps with | None -> - let f id = OnHyp (id,AllOccurrences,InHyp) in - List.map f (enum_hyps ()) + let f id = OnHyp (id,AllOccurrences,InHyp) in + List.map f (enum_hyps ()) | Some l -> - List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in + List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in if cl.concl_occs = NoOccurrences then hyps else OnConcl cl.concl_occs :: hyps |