Oh le joli bug dans le kernel:

Definissons un foncteur dependant de X et Y. Alors:

Module M
  : Funsig (X : T) Funsig (Y : T) Sig  End
  := Functor [Y:T] Functor [X:T] Struct  End

Notez les places de X et Y, a cause d'un fold_right qui aurait du etre
gauchiste. Etonnement, tout marchait tres bien en Coq, donc ce bug a
survecu discretement depuis l'ajout initial des modules. Avant que je 
n'essaie d'extraire un foncteur a deux arguments...



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8898 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 38587f7e5..c63762f54 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -269,10 +269,10 @@ let end_module l restype senv =
 	    mtb, Some mtb, cst
   in
   let mexpr = 
-    List.fold_right
-      (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb))
-      params
+    List.fold_left
+      (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb))
       (MEBstruct (modinfo.msid, List.rev senv.revstruct)) 
+      params
   in
   let mb = 
     { mod_expr = Some mexpr;