X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=34c601b3558ee15ba9d1bbe90038e7d4d2b4879d;hb=7fa3bd6487683920f34871688b357f08f67ebb3d;hp=0b3ec04a8176d53b9af64b0e384bab55f090b3fb;hpb=e13cffcb2d9b22f607034b15ec2e3abd47906602;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 0b3ec04a8..34c601b35 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -592,7 +592,9 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     !maxmeta, res 
   in
 
-  let res = demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left in
+  let res = 
+    demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left 
+  in
   if Utils.debug_res then check_res res "demod result";
   let newmeta, newtarget = 
     match res with