returns the right list of goals

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

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 69634a83051a10b71e9a2c482810f8d805acb4b4..65593985108f1e42d177074fb2c70957fe9cf6f1 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -858,15 +858,21 @@ exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
   let module C = Cic in
-  let rec aux table t1 t2 =
+  let rec aux ((table_l,table_r) as table) t1 t2 =
     match t1, t2 with
+    | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 = m2 -> table
+    | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 < m2 -> aux table t2 t1
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
-          (try
-            if List.assoc m1 table = m2 then table
-            else raise NotMetaConvertible
-          with Not_found -> 
-            try ignore(List.assoc m2 table);raise NotMetaConvertible
-            with Not_found -> (m1,m2)::table)
+        let m1_binding, table_l =
+          try List.assoc m1 table_l, table_l
+          with Not_found -> m2, (m1, m2)::table_l
+        and m2_binding, table_r =
+          try List.assoc m2 table_r, table_r
+          with Not_found -> m1, (m2, m1)::table_r
+        in
+        if (m1_binding <> m2) || (m2_binding <> m1) then
+          raise NotMetaConvertible
+        else table_l,table_r
     | C.Var (u1, ens1), C.Var (u2, ens2)
     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
         aux_ens table ens1 ens2
@@ -942,12 +948,12 @@ let meta_convertibility_eq eq1 eq2 =
     true
   else
     try
-      let table = meta_convertibility_aux [] left left' in
+      let table = meta_convertibility_aux ([],[]) left left' in
       let _ = meta_convertibility_aux table right right' in
       true
     with NotMetaConvertible ->
       try
-        let table = meta_convertibility_aux [] left right' in
+        let table = meta_convertibility_aux ([],[]) left right' in
         let _ = meta_convertibility_aux table right left' in
         true
       with NotMetaConvertible ->
@@ -960,7 +966,7 @@ let meta_convertibility t1 t2 =
     true
   else
     try
-      ignore(meta_convertibility_aux [] t1 t2);
+      ignore(meta_convertibility_aux ([],[]) t1 t2);
       true
     with NotMetaConvertible ->
       false
@@ -990,7 +996,8 @@ let equality_of_term bag proof term =
 
 let is_weak_identity eq = 
   let _,_,(_,left, right,_),_,_ = open_equality eq in
-   left = right (* doing metaconv here is meaningless *)
+   left = right 
+   (* doing metaconv here is meaningless *)
 ;;
 
 let is_identity (_, context, ugraph) eq =