diff options
| author | Jason Gross | 2018-08-15 11:03:42 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:54 -0400 |
| commit | 14626ba6a27323ac5a329c9f246bf64282738e5e (patch) | |
| tree | 86842d44eb30bb15f212a850c0dccf3862c09a2d /interp/notation.ml | |
| parent | 581bbbb23fcb488d5c1a10f360a6705a6792b2b1 (diff) | |
Add Numeral Notation GlobRef printing/parsing
Now we support using inductive constructors and section-local variables
as numeral notation printing and parsing functions.
I'm not sure that I got the econstr conversion right.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions