diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5962cf14d..1cfc50811 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -204,8 +204,15 @@ let print_modtype r = let dump_universes s = let output = open_out s in + let output_constraint kind left right = + let kind = match kind with + | `Lt -> "<" + | `Le -> "<=" + | `Eq -> "=" + in Printf.fprintf output "%s %s %s ;\n" left kind right + in try - Univ.dump_universes output (Global.universes ()); + Univ.dump_universes output_constraint (Global.universes ()); close_out output; msgnl (str ("Universes written to file \""^s^"\".")) with |