diff options
| author | Maxime Dénès | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /engine/universes.ml | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 70601987c3..ee9668433c 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -17,7 +17,7 @@ type universe_binders = UnivNames.universe_binders type univ_name_list = UnivNames.univ_name_list let pr_with_global_universes = UnivNames.pr_with_global_universes -let reference_of_level = UnivNames.reference_of_level +let reference_of_level = UnivNames.qualid_of_level let add_global_universe = UnivNames.add_global_universe |