diff options
| author | Jason Gross | 2018-09-19 09:47:16 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-09-19 18:43:02 -0400 |
| commit | ab0015c1c2fce185648da6c0364e6c3eb0515424 (patch) | |
| tree | 41f013e1304403a35db1ab19c1090d993735b0f2 /kernel/nativelambda.mli | |
| parent | 4888eb7ea720eaa34af8df2769fa300f1ea37173 (diff) | |
Fix Numeral Notations (3/4 - moving more stuff)
Move most of the rest of the stuff from numeral.ml to notation.ml. Now
that we use exceptions to print error messages, all of the
interpretation code for numeral notations can be moved to notation.ml.
This is commit 1/4 in the fix for #8401.
This is a pure cut/paste commit, modulo fixing name qualifications due
to moved things, and exposing some stuff in notation.mli (to be removed
in the next commit, where we finish the numeral notation reworking).
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions
