dolmen
dolmen copied to clipboard
Remove the Typer's addition builtins following the merge of Extensions/Plugins
With the notion of Extensions/Plugins from #214 , the additional_builtins of the Typer module is redundant and can be removed. However it would not be nice to users to remove it right away, and should instead be removed in a few versions (maybe after being deprecated ?).
Actually there is a difference between additional_builtins and extensions: additional_builtins give access to the state, while extensions do not. I'm not sure if this functionality is needed (in fact I think it is not -- in any case we don't use it in Alt-Ergo) but something to keep in mind maybe.