diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-26 08:28:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-26 08:28:27 +0000 |
| commit | 3a328ad8b23cdf9a6900f7335f1be7219a526916 (patch) | |
| tree | 2be1218a06bc0fee86d0ae947ab8e098bf8649d3 /pretyping | |
| parent | 050735fc533d7d8d4fa40f7762d789c6bdd04198 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d2290614c..ffd2fad54 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 |