diff options
| author | Hugo Herbelin | 2020-04-19 13:24:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-01 23:17:27 +0200 |
| commit | 653a06b843e380927b93e325dcbe1c339810406f (patch) | |
| tree | a14cdc52dd4f153477a42411480056349a1167e8 /doc/plugin_tutorial/Makefile | |
| parent | df8df4637dfb4106854554cc2ac94b4fdd565e80 (diff) | |
Changing fixpoint message "decreasing" -> "guarded".
This is to be compatible with the possibility of having non truly
recursive fixpoints.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions