From 8ac6145d5cc14823df48698a755d8adf048f026c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2017 12:22:32 +0200 Subject: [coqlib] Rebindable Coqlib namespace. We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias Co-authored-by: Maxime Dénès Co-authored-by: Vincent Laporte --- dev/doc/changes.md | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'dev/doc/changes.md') diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7e64f80ac5..32d457c6dd 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -19,6 +19,14 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 +Coqlib: + +- Most functions from the `Coqlib` module have been deprecated in favor of + `register_ref` and `lib_ref`. The first one is available through the + vernacular `Register` command; it binds a name to a constant. The second + command then enables to locate the registered constant through its name. The + name resolution is dynamic. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API -- cgit v1.2.3