Petite correction d'affichage de modules

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

1 files changed, 6 insertions, 2 deletions

diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index b20eb5f46..77209ac0d 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -74,7 +74,9 @@ and print_modtype locals mty = match mty with
 
 and print_sig locals msid sign = 
   let print_spec (l,spec) = (match spec with
-    | SPBconst _ -> str "Definition "
+    | SPBconst {const_body=Some _; const_opaque=false} -> str "Definition "
+    | SPBconst {const_body=None}
+    | SPBconst {const_opaque=true} -> str "Parameter "
     | SPBmind _ -> str "Inductive "
     | SPBmodule _ -> str "Module "
     | SPBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
@@ -83,7 +85,9 @@ and print_sig locals msid sign =
 
 and print_struct locals msid struc = 
   let print_body (l,body) = (match body with
-    | SEBconst _ -> str "Definition "
+    | SEBconst {const_body=Some _; const_opaque=false} -> str "Definition "
+    | SEBconst {const_body=Some _; const_opaque=true} -> str "Theorem "
+    | SEBconst {const_body=None} -> str "Parameter "
     | SEBmind _ -> str "Inductive "
     | SEBmodule _ -> str "Module "
     | SEBmodtype _ -> str "Module Type ") ++ str (string_of_label l)