Replace uses of Termops.dependent by more specific functions.

This is more efficient in general, because Termops.dependent doesn't take
advantage of the knowledge of its pattern argument.

1 files changed, 7 insertions, 0 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index b7531f6fc9..e9d17e3c59 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -851,6 +851,13 @@ let occur_meta_or_existential sigma c =
     | _ -> EConstr.iter sigma occrec c
   in try occrec c; false with Occur -> true
 
+let occur_metavariable sigma m c =
+  let rec occrec c = match EConstr.kind sigma c with
+  | Meta m' -> if Int.equal m m' then raise Occur
+  | _ -> EConstr.iter sigma occrec c
+  in
+  try occrec c; false with Occur -> true
+
 let occur_evar sigma n c =
   let rec occur_rec c = match EConstr.kind sigma c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur