aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorletouzey2008-11-15 22:08:52 +0000
committerletouzey2008-11-15 22:08:52 +0000
commitc2008aff6f227d9a84e45faa7ab8e421290c96d6 (patch)
tree9768eca66289ede08b6bcde04b553f18796ae30b /kernel
parentdbc7cc0632d15a48ee8c695b84099c96d940821d (diff)
Correct display of constraints for Print Universes "dumpfile"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1251d09f5d..58266a50f2 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -613,12 +613,12 @@ let dump_universes output g =
let u_str = string_of_univ_level u in
List.iter
(fun v ->
- Printf.fprintf output "%s > %s ;\n" u_str
+ Printf.fprintf output "%s < %s ;\n" u_str
(string_of_univ_level v))
lt;
List.iter
(fun v ->
- Printf.fprintf output "%s >= %s ;\n" u_str
+ Printf.fprintf output "%s <= %s ;\n" u_str
(string_of_univ_level v))
le
| Equiv (u,v) ->