]> matita.cs.unibo.it Git - helm.git/commitdiff
arguments of ProofEngineHelpers.replace swapped.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Jul 2005 15:08:57 +0000 (15:08 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Jul 2005 15:08:57 +0000 (15:08 +0000)
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