diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-19 17:20:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-19 17:35:59 +0100 |
| commit | a532777dcfc59128be2daa7cc74c7881a06f8cb3 (patch) | |
| tree | 97cde2983485df683a6a82780f1365c47aacadf7 /lib/genarg.mli | |
| parent | 7e6e533b148c9d57251388e9f1646a6829d10bfb (diff) | |
Adding a default object to generic argument registering mechanism.
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) : |