Termops: Adding functions local_occur_var_in_decl and occur_var_indirectly.

2 files changed, 19 insertions, 8 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 6d779e6a35..c51e753d46 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -803,23 +803,29 @@ let occur_evar sigma n c =
 
 let occur_in_global env id constr =
   let vars = vars_of_global env constr in
-  if Id.Set.mem id vars then raise Occur
+  Id.Set.mem id vars
 
 let occur_var env sigma id c =
   let rec occur_rec c =
     match EConstr.destRef sigma c with
-    | gr, _ -> occur_in_global env id gr
+    | gr, _ -> if occur_in_global env id gr then raise Occur
     | exception DestKO -> EConstr.iter sigma occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
+exception OccurInGlobal of GlobRef.t
+
+let occur_var_indirectly env sigma id c =
+  let var = GlobRef.VarRef id in
+  let rec occur_rec c =
+    match EConstr.destRef sigma c with
+    | gr, _ -> if not (GlobRef.equal gr var) && occur_in_global env id gr then raise (OccurInGlobal gr)
+    | exception DestKO -> EConstr.iter sigma occur_rec c
+  in
+  try occur_rec c; None with OccurInGlobal gr -> Some gr
+
 let occur_var_in_decl env sigma hyp decl =
-  let open NamedDecl in
-  match decl with
-    | LocalAssum (_,typ) -> occur_var env sigma hyp typ
-    | LocalDef (_, body, typ) ->
-        occur_var env sigma hyp typ ||
-        occur_var env sigma hyp body
+  NamedDecl.exists (occur_var env sigma hyp) decl
 
 let local_occur_var sigma id c =
   let rec occur c = match EConstr.kind sigma c with
@@ -828,6 +834,9 @@ let local_occur_var sigma id c =
   in
   try occur c; false with Occur -> true
 
+let local_occur_var_in_decl sigma hyp decl =
+  NamedDecl.exists (local_occur_var sigma hyp) decl
+
   (* returns the list of free debruijn indices in a term *)
 
 let free_rels sigma m =
diff --git a/engine/termops.mli b/engine/termops.mli
index 4e77aa9b3b..709fa361a9 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -92,12 +92,14 @@ val occur_meta_or_existential : Evd.evar_map -> constr -> bool
 val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
 val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
 val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
+val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option
 val occur_var_in_decl :
   env -> Evd.evar_map ->
   Id.t -> named_declaration -> bool
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
 val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
+val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool
 
 val free_rels : Evd.evar_map -> constr -> Int.Set.t