Added a new version of meta_convertibnility that returns the

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 30138b378f9eac358305f3ffbcc4170e05de44c7..e35918c689b805b0e6b4037133e001e9583abe8f 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -1026,7 +1026,6 @@ let meta_convertibility_eq eq1 eq2 =
         false
 ;;
 
-
 let meta_convertibility t1 t2 =
   if t1 = t2 then
     true
@@ -1038,6 +1037,32 @@ let meta_convertibility t1 t2 =
       false
 ;;
 
+let meta_convertibility_subst t1 t2 menv =
+  if t1 = t2 then
+    Some([])
+  else
+    try
+      let (l,_) = meta_convertibility_aux ([],[]) t1 t2 in
+      let subst =
+       List.map
+         (fun (x,y) ->
+            try 
+              let (_,c,t) = CicUtil.lookup_meta x menv in
+              let irl = 
+                CicMkImplicit.identity_relocation_list_for_metavariable c in
+              (x,(c,Cic.Meta(y,irl),t))
+            with CicUtil.Meta_not_found _ ->
+              try 
+                let (_,c,t) = CicUtil.lookup_meta y menv in
+                let irl =  
+                  CicMkImplicit.identity_relocation_list_for_metavariable c in
+                  (y,(c,Cic.Meta(x,irl),t))
+              with CicUtil.Meta_not_found _ -> assert false) l in   
+       Some subst
+    with NotMetaConvertible ->
+      None
+;;
+
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =