diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /engine/uState.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/uState.ml')
| -rw-r--r-- | engine/uState.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 0e3ecdbf5..81ab3dd66 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -295,15 +295,15 @@ let constrain_variables diff ctx = in { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } -let reference_of_level uctx = +let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) + try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - UnivNames.reference_of_level l + UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_reference (reference_of_level uctx l) + Libnames.pr_qualid (qualid_of_level uctx l) type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) |