fold.patch

diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index d10a358..7058e5f 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -18,6 +18,9 @@ open Libnames
 open Libobject
 open Mod_subst
 
+let rec list_fold_right_stackless f l init =
+  List.fold_left (fun x y -> f y x) init (List.rev l)
+
 (** {6 Inlining levels} *)
 
 (** Rigid / flexible module signature *)
@@ -607,7 +610,7 @@ let intern_args params =
 
 let check_sub mtb sub_mtb_l =
   (* The constraints are checked and forgot immediately : *)
-  ignore (List.fold_right
+  ignore (list_fold_right_stackless
             (fun sub_mtb env ->
                Environ.add_constraints
                  (Subtyping.check_subtypes env mtb sub_mtb) env)