aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorJason Gross2018-09-19 09:47:16 -0400
committerJason Gross2018-09-19 18:43:02 -0400
commitab0015c1c2fce185648da6c0364e6c3eb0515424 (patch)
tree41f013e1304403a35db1ab19c1090d993735b0f2 /kernel/nativelambda.mli
parent4888eb7ea720eaa34af8df2769fa300f1ea37173 (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