From 3a328ad8b23cdf9a6900f7335f1be7219a526916 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 26 Feb 2004 08:28:27 +0000
Subject: Inclusion des annotations de type des filtrages dans 'Set Printing
 All'

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

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d2290614c8..ffd2fad54a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -212,7 +212,7 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
   let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
   let consnargsl = Array.map List.length consnargs in
   let alias, aliastyp, newpred, pred = 
-    if synth_type & computable & bl <> [||] then
+    if (not !Options.raw_print) & synth_type & computable & bl <> [||] then
       Anonymous, None, None, None
     else
       let p = option_app detype p in
-- 
cgit v1.2.3