From 89e2121c4241178adc5510e774385e834716be97 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 9 Mar 2007 14:48:19 +0000
Subject: bug#1434 importing fonctor arguments, now it works.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9693 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 48829288fb..7dacbeabac 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -397,7 +397,7 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o =
        let binders_ast,argsexport =
         List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
-           (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+           (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast
              ([],[]) in
 	Declaremods.start_module Modintern.interp_modtype export
 	  id binders_ast mty_ast_o;
-- 
cgit v1.2.3