From c9f4643f733fbfa368cb4644f95b2e233d5ad973 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 5 Jun 2006 23:15:51 +0000 Subject: 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 --- kernel/safe_typing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel') 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; -- cgit v1.2.3