]> matita.cs.unibo.it Git - helm.git/commitdiff
changed universes merging order: euristic which improve performances
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 18 Jan 2006 10:42:01 +0000 (10:42 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 18 Jan 2006 10:42:01 +0000 (10:42 +0000)
helm/ocaml/cic/cicUniv.ml

index 669025ffef51d44fdf46c65c3a6f5703b1de6692..cfcbaf74178d2a2839d64b4bfede2e52abee19e3 100644 (file)
@@ -577,7 +577,7 @@ let merge_ugraphs u v =
                         (SOF.union v.one_s_eq v.eq_closure) x)))
         ) m1 m2
   in
-  merge_brutal u v
+  merge_brutal v u
 
 
 (*****************************************************************************)