]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUniv.ml
changed universes merging order: euristic which improve performances
[helm.git] / 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
 
 
 (*****************************************************************************)