diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 10 |
1 files changed, 10 insertions, 0 deletions
@@ -20,6 +20,16 @@ Vernacular commands - The undocumented and obsolete option "Set/Unset Boxed Definitions" has been removed, as well as syntaxes like "Boxed Fixpoint foo". +Module System + +- The inlining done during application of functors can now be controlled + more precisely. In addition to the "!F G" syntax preventing any inlining, + we can now use a priority level to select parameters to inline : + "<30>F X" means "only inline in F the parameters whose levels are <= 30". + The level of a parameter can be fixed by "Parameter Inline(30) foo". + When levels aren't given, the default value is 100. One can also use + the flag "Set Inline Level ..." to set a level. TODO: DOC! + Libraries - Creation of PArith, a subdirectory containing files about the positive type, |