From d1df4f36c4e304d6ed446d09b64d1b3bf34bac16 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 15 Oct 2008 15:07:10 +0000
Subject: Report des commits 11417 et 11437 de la v8.2

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11454 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/printmod.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index be73f573b5..596ce6b24b 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -90,7 +90,7 @@ and print_modtype locals mty =
       let s = (String.concat "." (List.map string_of_id idl)) in
       hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ 
 	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
-  | SEBwith(seb,With_module_body(idl,mp,_))->
+  | SEBwith(seb,With_module_body(idl,mp,_,_))->
       let s =(String.concat "." (List.map string_of_id idl)) in
       hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ 
 	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
@@ -102,7 +102,7 @@ and print_sig locals msid sign =
     | SFBconst {const_opaque=true} -> str "Parameter "
     | SFBmind _ -> str "Inductive "
     | SFBmodule _ -> str "Module "
-    | SFBalias (mp,_) -> str "Module "
+    | SFBalias (mp,_,_) -> str "Module "
     | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_spec sign
@@ -114,7 +114,7 @@ and print_struct locals msid struc =
     | SFBconst {const_body=None} -> str "Parameter "
     | SFBmind _ -> str "Inductive "
     | SFBmodule _ -> str "Module "
-    | SFBalias (mp,_) -> str "Module "
+    | SFBalias (mp,_,_) -> str "Module "
     | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_body struc
-- 
cgit v1.2.3