X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=7893ecba6142ef4a5934d3edc0fd18db3ec51a14;hb=25e80c6f83850854ed8e8e922fff4e467f8b9924;hp=30138b378f9eac358305f3ffbcc4170e05de44c7;hpb=b109559ac6795075508fd5c231a1bf2a3223031a;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 30138b378..7893ecba6 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/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
+	       (y,(c,Cic.Meta(x,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
+		   (x,(c,Cic.Meta(y,irl),t))
+	       with CicUtil.Meta_not_found _ -> assert false) l in   
+	Some subst
+    with NotMetaConvertible ->
+      None
+;;
+
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
@@ -1198,7 +1223,7 @@ let rec pp_proofterm name t context =
               when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
-              when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)->
+              when Pcre.pmatch ~pat:"eq_OF_eq" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] 
               when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->