diff options
Diffstat (limited to 'contrib/extraction/miniml.mli')
| -rw-r--r-- | contrib/extraction/miniml.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index a022d67d82..54a230881c 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -22,6 +22,7 @@ type ml_type = | Tapp of ml_type list | Tarr of ml_type * ml_type | Tglob of global_reference + | Texn of string | Tprop | Tarity |