diff options
Diffstat (limited to 'parsing/g_rsyntax.ml')
| -rw-r--r-- | parsing/g_rsyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 8f5aad33be..72f54721aa 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -175,7 +175,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] (* TODO: temporary hack *) -let make_path dir id = Libnames.encode_kn dir (id_of_string id) +let make_path dir id = Libnames.encode_con dir (id_of_string id) let glob_R = ConstRef (make_path rdefinitions "R") let glob_R1 = ConstRef (make_path rdefinitions "R1") |