From 9bbdee3c09c92654bb8937b9939a9b9c69c23d1d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Aug 2017 01:04:19 +0200
Subject: Introducing rebindable toplevel definitions.

---
 doc/ltac2.md | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/ltac2.md b/doc/ltac2.md
index d1c5c68494..5c057b3ead 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -218,7 +218,7 @@ Limitations: for now, deep pattern matching is not implemented yet.
 One can define a new global Ltac2 value using the following syntax.
 ```
 VERNAC ::=
-| "Ltac2" RECFLAG LIDENT ":=" TERM
+| "Ltac2" MUTFLAG RECFLAG LIDENT ":=" TERM
 ```
 
 For semantic reasons, the body of the Ltac2 definition must be a syntactical
@@ -227,6 +227,17 @@ values.
 
 If the `RECFLAG` is set, the tactic is expanded into a recursive binding.
 
+If the `MUTFLAG` is set, the definition can be redefined at a later stage. This
+can be performed through the following command.
+
+```
+VERNAC ::=
+| "Ltac2" "Set" QUALID ":=" TERM
+```
+
+Mutable definitions act like dynamic binding, i.e. at runtime, the last defined
+value for this entry is chosen. This is useful for global flags and the like.
+
 ## Reduction
 
 We use the usual ML call-by-value reduction, with an otherwise unspecified
-- 
cgit v1.2.3