From d446e47c39af1ae40a3072c188c81a978e95804c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 May 2006 15:17:51 +0000
Subject: [PATCH] fixed subsumption_aux - (merge_subst_if_possible no longer
 needed) - fixed case of use_unification = true

---
 components/tactics/paramodulation/indexing.ml | 45 ++++++++++---------
 1 file changed, 24 insertions(+), 21 deletions(-)

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index d68c6d651..fd3caa345 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -409,21 +409,25 @@ let find_all_matches
   returns true if target is subsumed by some equality in table
 *)
 let subsumption_aux use_unification env table target = 
-  (* 
-  let print_res l =
-    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
-    ((pos,equation),_)) -> Inference.string_of_equality equation)l))
-  in
-  *)
+(*  let print_res l =*)
+(*    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
+(*    ((pos,equation),_)) -> Equality.string_of_equality equation)l))*)
+(*  in*)
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let metasenv, context, ugraph = env in
   let metasenv = tmetas in
+  let predicate, unif_fun = 
+    if use_unification then
+      Unification, Inference.unification
+    else
+      Matching, Inference.matching
+  in
   let leftr =
     match left with
-    | Cic.Meta _ -> []   
+    | Cic.Meta _ when not use_unification -> []   
     | _ ->
-        let leftc = get_candidates Matching table left in
-        find_all_matches ~unif_fun:Inference.matching
+        let leftc = get_candidates predicate table left in
+        find_all_matches ~unif_fun
           metasenv context ugraph 0 left ty leftc
   in
 (*  print_res leftr;*)
@@ -436,16 +440,14 @@ let subsumption_aux use_unification env table target =
           let subst', menv', ug' =
             let t1 = Unix.gettimeofday () in
             try
-              let r = 
-                if use_unification then
-                  Inference.unification metasenv m context what other ugraph
-                else
-                  Inference.matching metasenv m context what other ugraph
-              in
+              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 as e ->
+            with 
+              | Inference.MatchingFailure 
+              | CicUnification.UnificationFailure _ as e ->
               let t2 = Unix.gettimeofday () in
               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
               raise e
@@ -453,18 +455,19 @@ let subsumption_aux use_unification env table target =
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok what tl
           | Some s -> Some (s, equation))
-        with Inference.MatchingFailure ->
-          ok what tl
+        with 
+        | Inference.MatchingFailure 
+        | CicUnification.UnificationFailure _ -> ok what tl
   in
   match ok right leftr with
   | Some _ as res -> res
   | None -> 
       let rightr =
         match right with
-          | Cic.Meta _ -> [] 
+          | Cic.Meta _ when not use_unification -> [] 
           | _ ->
-              let rightc = get_candidates Matching table right in
-                find_all_matches ~unif_fun:Inference.matching
+              let rightc = get_candidates predicate table right in
+                find_all_matches ~unif_fun
                   metasenv context ugraph 0 right ty rightc
       in
 (*        print_res rightr;*)
-- 
2.39.2