From df2ff3a99afc7d8bb741d2623a12366ea6ca8e0b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 8 Dec 2006 12:27:21 +0000
Subject: Pas d'escamotage des noms réservés si Set Printing All actibvé

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

diff --git a/interp/reserve.ml b/interp/reserve.ml
index 85f1885990..39ba6d6fd5 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -84,7 +84,7 @@ let rec unloc = function
 let anonymize_if_reserved na t = match na with
   | Name id as na ->
       (try 
-	if unloc t = find_reserved_type id
+	if not !Options.raw_print & unloc t = find_reserved_type id
 	then RHole (dummy_loc,Evd.BinderType na)
 	else t
       with Not_found -> t)
-- 
cgit v1.2.3