From fc8e1e2ad5b37b4c60f9d73cda368f7808679f6d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 17:07:53 +0000
Subject: [PATCH] fixed metaconvertibility that was completely wrong.
 is_identity and is_weak_identity fixed accordingly

---
 .../tactics/paramodulation/equality.ml        | 41 ++++++-------------
 1 file changed, 12 insertions(+), 29 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index b229cc05f..69634a830 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -858,31 +858,15 @@ 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 t1 t2 =
     match t1, t2 with
     | 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
-        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 (
-          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
-        )
+          (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)
     | 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 +942,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 +960,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,13 +990,12 @@ 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)) *)
+  (* doing metaconv here is meaningless *)
   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
 ;;
 
-- 
2.39.2