Change (or better define) the order of hints premises.

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index cc103a8ab6036349cf5893da12a0076773b49cc6..deb743d90b8fd20a63f292d79ffe350adeefe317 100644 (file)
--- 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)