Moving function about locs in locusops.

3 files changed, 33 insertions, 26 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
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index a086a6f58..73d13c0bc 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -35,3 +35,10 @@ val is_nowhere : 'a clause_expr -> bool
 
 val simple_clause_of : (unit -> Id.t list) -> clause -> simple_clause
 val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause
+
+(** Miscellaneous functions *)
+
+val occurrences_of_hyp : Id.t -> Id.t clause_expr ->
+  occurrences * hyp_location_flag
+val occurrences_of_goal : 'a clause_expr -> occurrences
+val in_every_hyp : 'a clause_expr -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2a6fd6fe7..7544ba37a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1311,26 +1311,6 @@ let iter_fail f a =
 (* make_abstraction: a variant of w_unify_to_subterm which works on
    contexts, with evars, and possibly with occurrences *)
 
-let out_arg = function
-  | Misctypes.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | Misctypes.ArgArg x -> x
-
-let occurrences_of_hyp id cls =
-  let rec hyp_occ = function
-      [] -> None
-    | ((occs,id'),hl)::_ when Id.equal id id' ->
-        Some (occurrences_map (List.map out_arg) occs, hl)
-    | _::l -> hyp_occ l in
-  match cls.onhyps with
-      None -> Some (AllOccurrences,InHyp)
-    | Some l -> hyp_occ l
-
-let occurrences_of_goal cls =
-  if cls.concl_occs == NoOccurrences then None
-  else Some (occurrences_map (List.map out_arg) cls.concl_occs)
-
-let in_every_hyp cls = Option.is_empty cls.onhyps
-
 let indirectly_dependent c d decls =
   not (isVar c) &&
     (* This test is not needed if the original term is a variable, but
@@ -1432,7 +1412,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
   let mkvarid () = mkVar id in
   let compute_dependency _ (hyp,_,_ as d) depdecls =
     match occurrences_of_hyp hyp occs with
-    | None ->
+    | NoOccurrences, InHyp ->
         if indirectly_dependent c d depdecls then
           (* Told explicitly not to abstract over [d], but it is dependent *)
           let id' = indirect_dependency d depdecls in
@@ -1441,7 +1421,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
             ++ str ".")
         else
           depdecls
-    | Some ((AllOccurrences, InHyp) as occ) ->
+    | (AllOccurrences, InHyp) as occ ->
         let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
         if Context.eq_named_declaration d newdecl
            && not (indirectly_dependent c d depdecls)
@@ -1451,14 +1431,13 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc
           else depdecls
         else
           newdecl :: depdecls
-    | Some occ ->
+    | occ ->
         replace_term_occ_decl_modulo occ test mkvarid d :: depdecls in
   try
     let depdecls = fold_named_context compute_dependency env ~init:[] in
     let ccl = match occurrences_of_goal occs with
-      | None -> concl
-      | Some occ ->
-          replace_term_occ_modulo occ test mkvarid concl
+      | NoOccurrences -> concl
+      | occ -> replace_term_occ_modulo occ test mkvarid concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in