From 39471db28724f5720868f7a7d1488d81d190ee60 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 23 May 2019 13:52:23 +0200 Subject: Update `Bind Scope` documentation to reflect 3d09e39dd423d81c6af3e991d5b282ea8608646b The commit mentioned above changed the semantics of `Bind Scope` to a dynamic binding behavior. It forgot to update the documentation. Fixes #10064 --- doc/sphinx/user-extensions/syntax-extensions.rst | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3710c0af9d..ec5da36b5e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1141,10 +1141,10 @@ Binding types of arguments to an interpretation scope When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it - to this type. When a scope ``scope`` is bound to a type ``type``, any new function - defined later on gets its arguments of type ``type`` interpreted by default in - scope ``scope`` (this default behavior can however be overwritten by explicitly - using the command :cmd:`Arguments `). + to this type. When a scope ``scope`` is bound to a type ``type``, any function + gets its arguments of type ``type`` interpreted by default in scope scope + (this default behavior can however be overwritten by explicitly using the + command :cmd:`Arguments `). Whether the argument of a function has some type ``type`` is determined statically. For instance, if ``f`` is a polymorphic function of type @@ -1172,6 +1172,11 @@ Binding types of arguments to an interpretation scope Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). + .. note:: When active, a bound scope has effect on all defined functions + (even if they are defined after the `Bind Scope` directive), except + if argument scopes were assigned explicitly using the + :cmd:`Arguments ` command. + .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local effect on interpretation. See the next section. -- cgit v1.2.3 From 4a5f6c1ee8c6f6dfe934b63ff5a4ec950d3efe55 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 23 May 2019 16:39:39 +0200 Subject: Update doc/sphinx/user-extensions/syntax-extensions.rst Co-Authored-By: Théo Zimmermann --- doc/sphinx/user-extensions/syntax-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ec5da36b5e..b8e2230b1b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1141,7 +1141,7 @@ Binding types of arguments to an interpretation scope When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it - to this type. When a scope ``scope`` is bound to a type ``type``, any function + to this type. When a scope :token:`scope` is bound to a type :token:`type`, any function gets its arguments of type ``type`` interpreted by default in scope scope (this default behavior can however be overwritten by explicitly using the command :cmd:`Arguments `). -- cgit v1.2.3 From f08df3055c110a3ae5b708a384fe681e170dfbba Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 23 May 2019 16:39:56 +0200 Subject: Update doc/sphinx/user-extensions/syntax-extensions.rst Co-Authored-By: Théo Zimmermann --- doc/sphinx/user-extensions/syntax-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index b8e2230b1b..70c41d5be0 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1142,7 +1142,7 @@ Binding types of arguments to an interpretation scope When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it to this type. When a scope :token:`scope` is bound to a type :token:`type`, any function - gets its arguments of type ``type`` interpreted by default in scope scope + gets its arguments of type :token:`type` interpreted by default in scope :token:`scope` (this default behavior can however be overwritten by explicitly using the command :cmd:`Arguments `). -- cgit v1.2.3 From 15891b8179a82884bf72df8c7d7d696d29f53434 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 23 May 2019 16:40:05 +0200 Subject: Update doc/sphinx/user-extensions/syntax-extensions.rst Co-Authored-By: Théo Zimmermann --- doc/sphinx/user-extensions/syntax-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 70c41d5be0..06259e4db0 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1173,7 +1173,7 @@ Binding types of arguments to an interpretation scope Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). .. note:: When active, a bound scope has effect on all defined functions - (even if they are defined after the `Bind Scope` directive), except + (even if they are defined after the :cmd:`Bind Scope` directive), except if argument scopes were assigned explicitly using the :cmd:`Arguments ` command. -- cgit v1.2.3