diff options
| author | Hugo Herbelin | 2017-09-24 10:27:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-12-14 15:57:51 +0100 |
| commit | c248228f5e910e19114e827661abb255c77a2b01 (patch) | |
| tree | 4bb1ba77ed70893c67015e46599bf38ac70d8ad0 /plugins/syntax/string_syntax.ml | |
| parent | 63d582c6cd12bc3f8134a5aa9e3bdbca0dd2e9ca (diff) | |
Cosmetic: using "types" rather "constr" in some types of term.mli.
This enforces the intended meaning of the corresponding functions
(prod_appvect*/prod_applist*).
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions