From 793347ab8325696d413ab3a7016228130734e697 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 13 Dec 2002 13:23:22 +0000
Subject: possibilité de faire Print M avec M module ou modtype au lieu de
 Print Module et Print Module Type

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

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4621f1bb27..1aa337373f 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -464,6 +464,10 @@ let print_name r =
   try
     let kn = Nametab.locate_syntactic_definition qid in
     print_syntactic_def " = " kn
+  with Not_found ->
+  try print_module true (Nametab.locate_module qid)
+  with Not_found -> 
+  try print_modtype (Nametab.locate_modtype qid)
   with Not_found ->
     user_err_loc
       (loc,"print_name",pr_qualid qid ++ spc () ++ str "not a defined object")
-- 
cgit v1.2.3