aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorcorbinea2008-02-14 13:59:33 +0000
committercorbinea2008-02-14 13:59:33 +0000
commit921f0ef22fcd79e69486e0aec75e57f68dce661e (patch)
treea8a62246fdbb6363e1f3e1a39d5b8d5ca1c27fcd /parsing
parentbb3560885d943baef87b7f99a5d646942f0fb288 (diff)
Added default canonical structures (see example in test-suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/prettyp.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 6712af8b99..2eb22b177d 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -744,7 +744,9 @@ let print_path_between cls clt =
let print_canonical_projections () =
prlist_with_sep pr_fnl (fun ((r1,r2),o) ->
- pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
+ (match r2 with Some sr2 -> pr_global sr2 | None -> str " _") ++
+ str " <- " ++
+ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
(canonical_projections ())
(*************************************************************************)