]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/saturation.ml
added homepage URL, now we have one
[helm.git] / helm / ocaml / paramodulation / saturation.ml
index 13bb5714a6678910810168d10d5a684816021eca..413c7b15ea7bd760ed301b64f46d025336c3a646 100644 (file)
@@ -1170,7 +1170,7 @@ let saturate dbd (proof, goal) =
                  (string_of_bool
                     (fst (CicReduction.are_convertible
                             context type_of_goal ty ug))));
-            let equality_for_replace t1 i =
+            let equality_for_replace i t1 =
               match t1 with
               | C.Meta (n, _) -> n = i
               | _ -> false