aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2005-02-12 18:23:06 +0000
committerherbelin2005-02-12 18:23:06 +0000
commit66dc6ecf0a1765245a6ef3b82921df513bccab94 (patch)
tree13403df3ce2db873aa8b7056099531ce218222a9
parent3c5903f1c2057c98ff2d1864d1d6727040b5f8fc (diff)
Nouvelle mouture Print Canonical Structures
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6714 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--parsing/prettyp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 50347df033..a358301e5b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -630,7 +630,7 @@ let print_path_between cls clt =
let print_canonical_structures () =
prlist_with_sep pr_fnl (fun ((r1,r2),o) ->
- prterm o.o_DEF ++ str ": " ++ pr_global r1 ++ str " >-> " ++ pr_global r2)
+ pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ prterm o.o_DEF ++ str " )")
(canonical_structures ())
(*************************************************************************)