diff options
| author | Pierre-Marie Pédrot | 2021-03-06 23:32:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-12 13:39:03 +0100 |
| commit | 285419e99996354ad2056bc38725c7a592124e7c (patch) | |
| tree | e4501ef5d6ccfa34643fde049e98fd156830bf54 /doc/plugin_tutorial/tuto2 | |
| parent | 93ea9206cbf29617feb23646f95e794b11e87793 (diff) | |
Further simplification of the term replacing code.
We factorize the code for replace and subst, since it seems there is no
reason to keep them separate, not even performance. Some static invariants are
made explicit in the API.
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions