diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-13 11:40:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-13 11:40:41 +0100 |
| commit | 013e161b7362aefb6a7a9117999e415cce3db9c2 (patch) | |
| tree | 01c7f1290dd84943d46d576563e7ad5e1d1b7c4e | |
| parent | 74682bb27da074fedc115238f3085baaccf12d73 (diff) | |
More in CHANGES about local definitions
| -rw-r--r-- | CHANGES | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -47,7 +47,11 @@ Vernacular commands doing "destruct". - The "Open Scope" command can now be given also a delimiter (e.g. Z). - The "Definition" command now allows the "Local" modifier, allowing - for non-importable definitions. + for non-importable definitions. The same goes for "Axiom" and "Parameter". +- Section-specific commands such as "Let" (resp. "Variable", "Hypothesis") used + out of a section now behave like the corresponding "Local" command, i.e. + "Local Definition" (resp. "Local Parameter", "Local Axiom"). (potential source + of rare incompatibilities). - The "Let" command can now define local (co)fixpoints. - Command "Search" has been renamed into "SearchHead". The command name "Search" now behaves like former "SearchAbout". The latter name |