diff options
Diffstat (limited to 'lib/genarg.mli')
| -rw-r--r-- | lib/genarg.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli index f275b0d00..6eea3ac92 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -227,6 +227,9 @@ sig val name : string (** A name for such kind of manipulation, e.g. [interp]. *) + + val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option + (** A generic object when there is no registered object for this type. *) end module Register (M : GenObj) : |