More efficient variable membership check for Logic.move.

Instead of repeatedly crawling the same hypothesis again and again we
only iter the term once.

1 files changed, 13 insertions, 0 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index d60aa69ccb..a0248fa01b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -839,6 +839,16 @@ let occur_var env sigma id c =
   in
   try occur_rec c; false with Occur -> true
 
+let occur_vars env sigma ids c =
+  let rec occur_rec c =
+    match EConstr.destRef sigma c with
+    | gr, _ ->
+      let vars = vars_of_global env gr in
+      if not (Id.Set.is_empty (Id.Set.inter ids vars)) 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 =
@@ -853,6 +863,9 @@ let occur_var_indirectly env sigma id c =
 let occur_var_in_decl env sigma hyp decl =
   NamedDecl.exists (occur_var env sigma hyp) decl
 
+let occur_vars_in_decl env sigma hyps decl =
+  NamedDecl.exists (occur_vars env sigma hyps) decl
+
 let local_occur_var sigma id c =
   let rec occur c = match EConstr.kind sigma c with
   | Var id' -> if Id.equal id id' then raise Occur