diff options
| author | Hugo Herbelin | 2017-04-02 11:21:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-09 11:52:17 +0200 |
| commit | 1a43fda0dc9bb8d100808426980446353f8f1ae3 (patch) | |
| tree | 5907412903414e3c21d718a70dc0d377a3589b1a /kernel/nativevalues.ml | |
| parent | 2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff) | |
Removing internal support for accepting "{struct x}" and co in "Theorem with".
There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions