diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-09 23:24:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 2194292dbe88674fd9a606bb22f28d332f670f77 (patch) | |
| tree | 21c2e91b13a5de21856554b17f5dfaa61101e253 /toplevel/record.ml | |
| parent | af7a9a4e44739968b68aeb1cb0a1f70a1aa34e88 (diff) | |
Revise syntax of Hint Cut
As noticed by C. Cohen it was confusingly different from standard
notation.
Diffstat (limited to 'toplevel/record.ml')
0 files changed, 0 insertions, 0 deletions