Adding a default object to generic argument registering mechanism.

2 files changed, 8 insertions, 1 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 3fb8155106..58dfbc91a1 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 f275b0d004..6eea3ac926 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) :