aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt22
-rw-r--r--dev/top_printers.ml2
2 files changed, 23 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 92ea62b5e4..ebbcb46ce9 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,28 @@
= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
=========================================
+** Cleaning in libnames/nametab interfaces
+
+Functions:
+
+dirpath_prefix -> pop_dirpath
+extract_dirpath_prefix pop_dirpath_n
+extend_dirpath -> add_dirpath_suffix
+qualid_of_sp -> qualid_of_path
+pr_sp -> pr_path
+make_short_qualid -> qualid_of_ident
+sp_of_syntactic_definition -> path_of_syntactic_definition
+sp_of_global -> path_of_global
+id_of_global -> basename_of_global
+absolute_reference -> global_of_path
+locate_syntactic_definition -> locate_syndef
+path_of_syntactic_definition -> path_of_syndef
+push_syntactic_definition -> push_syndef
+
+Types:
+
+section_path -> full_path
+
** Cleaning in parsing extensions (commit 12108)
Many moves and renamings, one new file (Extrawit, that contains wit_tactic).
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e3addd6f04..b35d5d4899 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -46,7 +46,7 @@ let ppdir dir = pp (pr_dirpath dir)
let ppmp mp = pp(str (string_of_mp mp))
let ppcon con = pp(pr_con con)
let ppkn kn = pp(pr_kn kn)
-let ppsp sp = pp(pr_sp sp)
+let ppsp sp = pp(pr_path sp)
let ppqualid qid = pp(pr_qualid qid)
let ppclindex cl = pp(Classops.pr_cl_index cl)