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 /vernac/metasyntax.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 'vernac/metasyntax.ml')
-rw-r--r-- | vernac/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8f64f5519..da14358ef 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1449,7 +1449,7 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = CAst.make @@ CRef (CAst.make @@ Ident (Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None) let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; |