many checks guarded with if Utils.debug_metas

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 8f4e5485174433bcbbb8b55b75610969d1620a76..7ee7d6b162d5f439b5fad8a45917bf57c9e3f75a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -820,7 +820,8 @@ let find_all_subsumed bag env table (goalproof,menv,ty) =
          (fun (subst, equality, swapped) (bag,acc) ->
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
              let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
-             Indexing.check_for_duplicates cicmenv "from subsumption";
+             if Utils.debug_metas then
+               Indexing.check_for_duplicates cicmenv "from subsumption";
              let bag, p =
               if swapped then
                  Equality.symmetric bag eq_ty l id uri m