diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index 6173849b1..1695eb3da 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -2387,12 +2387,16 @@ module NormMp = struct
 
   let globals env m mp =
     let us = mod_use env mp in
-    let l =
-      Sid.fold (fun id l -> f_glob id m :: l) us.us_gl [] in
-    let l =
-      Mx.fold
-        (fun xp ty l -> f_pvar (EcTypes.pv_glob xp) ty m :: l) us.us_pv l in
-    f_tuple l
+
+    let locals = Sid.elements us.us_gl in
+    let locals = List.sort EcIdent.id_ntr_compare locals in
+    let locals = List.map (fun id -> f_glob id m) locals in
+
+    let pv = Mx.bindings us.us_pv in
+    let pv = List.sort (fun (xp1, _) (xp2, _) -> x_ntr_compare xp1 xp2) pv in
+    let pv = List.map (fun (xp, ty) -> f_pvar (pv_glob xp) ty m) pv in
+
+    f_tuple (locals @ pv)
 
   let norm_glob env m mp = globals env m mp