From 457cee4345ab4ad6b6624a6886841fd0b0739b2a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 30 Jan 2020 08:18:49 +0100 Subject: Allow to rebind the old value of a mutable Ltac2 entry. --- doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst | 6 ++++++ doc/sphinx/proof-engine/ltac2.rst | 4 +++- 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst (limited to 'doc') diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst new file mode 100644 index 0000000000..0dd0fed4e2 --- /dev/null +++ b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to + give a name to the old value so as to be able to reuse it inside the + new one + (`#11503 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 35062e0057..0eb7ac6bb2 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -226,12 +226,14 @@ Ltac Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). -.. cmd:: Ltac2 Set @qualid := @ltac2_term +.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term :name: Ltac2 Set This command redefines a previous ``mutable`` definition. 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. + The previous value of the binding can be optionally accessed using the `as` + binding syntax. Reduction ~~~~~~~~~ -- cgit v1.2.3