diff options
| author | Pierre-Marie Pédrot | 2015-10-06 19:09:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-06 20:09:06 +0200 |
| commit | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (patch) | |
| tree | baee8c0b023277d43366996685503c9d1f855413 /toplevel | |
| parent | c4db6fc1086d984fd983ff9a6797ad108d220b98 (diff) | |
Splitting kernel universe code in two modules.
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c07c756c01..229f3acfdd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -347,7 +347,7 @@ let dump_universes_gen g s = end in try - Univ.dump_universes output_constraint g; + UGraph.dump_universes output_constraint g; close (); msg_info (str "Universes written to file \"" ++ str s ++ str "\".") with reraise -> @@ -357,7 +357,7 @@ let dump_universes_gen g s = let dump_universes sorted s = let g = Global.universes () in - let g = if sorted then Univ.sort_universes g else g in + let g = if sorted then UGraph.sort_universes g else g in dump_universes_gen g s (*********************) @@ -1640,12 +1640,12 @@ let vernac_print = function | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) | PrintUniverses (b, None) -> let univ = Global.universes () in - let univ = if b then Univ.sort_universes univ else univ in + let univ = if b then UGraph.sort_universes univ else univ in let pr_remaining = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in - msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) |