diff options
| author | Pierre-Marie Pédrot | 2017-08-27 01:04:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-27 16:29:52 +0200 |
| commit | 9bbdee3c09c92654bb8937b9939a9b9c69c23d1d (patch) | |
| tree | b3d1c29ff58ce67cdf11123b48175098100f0354 /doc | |
| parent | 7f562a9539522e56004596a751758a08cee798b1 (diff) | |
Introducing rebindable toplevel definitions.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ltac2.md | 13 |
1 files changed, 12 insertions, 1 deletions
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 |