removed equality_retrieval

[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 b229cc05fc2102c396ab87af6de2e51a747022bb..7123c134a93a98056655f6cee83e55600b559945 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -858,10 +858,11 @@ exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
   let module C = Cic in
-  let rec aux ((table_l, table_r) as 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) ->
-        let tl1, tl2 = [],[] in
         let m1_binding, table_l =
           try List.assoc m1 table_l, table_l
           with Not_found -> m2, (m1, m2)::table_l
@@ -871,18 +872,7 @@ let meta_convertibility_aux table t1 t2 =
         in
         if (m1_binding <> m2) || (m2_binding <> m1) then
           raise NotMetaConvertible
-        else (
-          try
-            List.fold_left2
-              (fun res t1 t2 ->
-                 match t1, t2 with
-                 | None, Some _ | Some _, None -> raise NotMetaConvertible
-                 | None, None -> res
-                 | Some t1, Some t2 -> (aux res t1 t2))
-              (table_l, table_r) tl1 tl2
-          with Invalid_argument _ ->
-            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
@@ -958,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 ->
@@ -976,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
@@ -1006,14 +996,16 @@ let equality_of_term bag proof term =
 
 let is_weak_identity eq = 
   let _,_,(_,left, right,_),_,_ = open_equality eq in
-  left = right || meta_convertibility left right 
+   left = right 
+   (* doing metaconv here is meaningless *)
 ;;
 
 let is_identity (_, context, ugraph) eq = 
   let _,_,(ty,left,right,_),menv,_ = open_equality eq in
-  left = right ||
-  (* (meta_convertibility left right)) *)
-  fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+  (* doing metaconv here is meaningless *)
+  left = right
+(*   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ *   *)
 ;;