X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=deb743d90b8fd20a63f292d79ffe350adeefe317;hb=7d7f1e8403bebcfc759d0955bd2f5a4837c414b2;hp=cc103a8ab6036349cf5893da12a0076773b49cc6;hpb=e8fbe5898b3214a5b0c4d48e8c9d1ee55f3415cc;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index cc103a8ab..deb743d90 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -694,7 +694,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
                 List.fold_left 
                   (fun (metasenv, subst) (x,y) ->
                      unify rdb test_eq_only metasenv subst context x y false)
-                  (metasenv, subst) premises
+                  (metasenv, subst) (List.rev premises)
               in
               pp(lazy("FUNZIONA!"));
               Some (metasenv, subst)