From 19d7e0ef6f45d918f5a2ebdbb4e634a4e4580cb2 Mon Sep 17 00:00:00 2001
From: coq
Date: Thu, 8 May 2003 14:33:34 +0000
Subject: Petite correction d'affichage de modules

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

diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index b20eb5f46a..77209ac0d4 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)
-- 
cgit v1.2.3