X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=7123c134a93a98056655f6cee83e55600b559945;hb=c049b167b6a59e7a1e755c0f5a4bc00ce0826c48;hp=69634a83051a10b71e9a2c482810f8d805acb4b4;hpb=3c14f9280a8a843b3caefe67df27272f9afe0a81;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 69634a830..7123c134a 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/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,13 +996,16 @@ 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 = 
   let _,_,(ty,left,right,_),menv,_ = open_equality eq in
   (* doing metaconv here is meaningless *)
-  fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+  left = right
+(*   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ *   *)
 ;;