is_identity -> is_weak_identity

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 0b3ec04a8176d53b9af64b0e384bab55f090b3fb..34c601b3558ee15ba9d1bbe90038e7d4d2b4879d 100644 (file)
--- 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