existential variables in goal supported

[helm.git] / components / tactics / paramodulation / indexing.ml

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index fd3caa345963398b86ef482ef920e57164f39e12..2c560cb55b7e7cf5a975d1a0fdb0e6b3337907d1 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -437,20 +437,9 @@ let subsumption_aux use_unification env table target =
         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
         try
           let other = if pos = Utils.Left then r else l in
+          let what' = Subst.apply_subst subst what in
           let subst', menv', ug' =
-            let t1 = Unix.gettimeofday () in
-            try
-              let other = Subst.apply_subst subst other in
-              let r = unif_fun metasenv m context what other ugraph in 
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-              r
-            with 
-              | Inference.MatchingFailure 
-              | CicUnification.UnificationFailure _ as e ->
-              let t2 = Unix.gettimeofday () in
-              match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-              raise e
+            unif_fun metasenv m context what' other ugraph
           in
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok what tl