diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/locusops.ml | 14 | ||||
| -rw-r--r-- | pretyping/locusops.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
3 files changed, 13 insertions, 7 deletions
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 7e825b6c2..cc19f01f8 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -102,7 +102,13 @@ let occurrences_of_goal cls = let in_every_hyp cls = Option.is_empty cls.onhyps -let has_selected_occurrences cls = - cls.concl_occs != AllOccurrences || - not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) -> - occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps) +let clause_with_generic_occurrences cls = + let hyps = match cls.onhyps with + | None -> true + | Some hyps -> + List.for_all + (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in + let concl = match cls.concl_occs with + | AllOccurrences | NoOccurrences -> true + | _ -> false in + hyps && concl diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index c1bf2d9ea..1d7c6b72e 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -42,4 +42,4 @@ val occurrences_of_hyp : Id.t -> clause -> (occurrences * hyp_location_flag) val occurrences_of_goal : clause -> occurrences val in_every_hyp : clause -> bool -val has_selected_occurrences : clause -> bool +val clause_with_generic_occurrences : 'a clause_expr -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3f2963bfe..3f6a4e307 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1468,7 +1468,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = else x in - let likefirst = not (has_selected_occurrences occs) in + let likefirst = clause_with_generic_occurrences occs in let mkvarid () = mkVar id in let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) = match occurrences_of_hyp hyp occs with @@ -1508,7 +1508,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = in let lastlhyp = if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in - (id,sign,depdecls,lastlhyp,ccl,out test) + (id,sign,depdecls,lastlhyp,ccl,out test) with SubtermUnificationError e -> raise (PretypeError (env,sigma,CannotUnifyOccurrences e)) |