diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/genarg.ml | 6 | ||||
| -rw-r--r-- | lib/genarg.mli | 3 |
2 files changed, 8 insertions, 1 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index 3fb815510..58dfbc91a 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -194,6 +194,7 @@ module type GenObj = sig type ('raw, 'glb, 'top) obj val name : string + val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option end module Register (M : GenObj) = @@ -213,7 +214,10 @@ struct let get_obj0 name = try String.Map.find name !arg0_map with Not_found -> - Errors.anomaly (str M.name ++ str " function not found: " ++ str name) + match M.default (ExtraArgType name) with + | None -> + Errors.anomaly (str M.name ++ str " function not found: " ++ str name) + | Some obj -> obj (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) 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) : |