2 files changed, 33 insertions, 15 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml
index b4f87d96b3..0d640640b3 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -64,23 +64,10 @@ type 'a with_ebindings = 'a * open_constr bindings
 
 type 'a generic_argument = argument_type * Obj.t
 
-let dyntab = ref ([] : string list)
-
 type rlevel
 type glevel
 type tlevel
 
-type ('a,'b) abstract_argument_type = argument_type
-
-let create_arg s =
-  if List.mem s !dyntab then
-    anomaly ("Genarg.create: already declared generic argument " ^ s);
-  dyntab := s :: !dyntab;
-  let t = ExtraArgType s in
-  (t,t,t)
-
-let exists_argtype s = List.mem s !dyntab
-
 type intro_pattern_expr =
   | IntroOrAndPattern of or_and_intro_pattern_expr
   | IntroWildcard
@@ -260,3 +247,32 @@ let unquote x = x
 type an_arg_of_this_type = Obj.t
 
 let in_generic t x = (t, Obj.repr x)
+
+let dyntab = ref ([] : (string * glevel generic_argument option) list)
+
+type ('a,'b) abstract_argument_type = argument_type
+
+let create_arg v s =
+  if List.mem_assoc s !dyntab then
+    anomaly ("Genarg.create: already declared generic argument " ^ s);
+  let t = ExtraArgType s in
+  dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
+  (t,t,t)
+
+let exists_argtype s = List.mem_assoc s !dyntab
+
+let default_empty_argtype_value s = List.assoc s !dyntab
+
+let default_empty_value t =
+  let rec aux = function
+  | List0ArgType _ -> Some (in_gen t [])
+  | OptArgType _ -> Some (in_gen t None)
+  | PairArgType(t1,t2) ->
+      (match aux t1, aux t2 with
+      | Some (_,v1), Some (_,v2) -> Some (in_gen t (v1,v2))
+      | _ -> None)
+  | ExtraArgType s -> default_empty_argtype_value s
+  | _ -> None in
+  match aux t with
+  | Some v -> Some (out_gen t v)
+  | None -> None
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 9c47c691a9..43cd73aedb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -257,7 +257,8 @@ val app_pair :
 
 (** create a new generic type of argument: force to associate
    unique ML types at each of the three levels *)
-val create_arg : string ->
+val create_arg : 'globa option ->
+    string ->
       ('a,tlevel) abstract_argument_type
       * ('globa,glevel) abstract_argument_type
       * ('rawa,rlevel) abstract_argument_type
@@ -299,7 +300,6 @@ val in_gen :
 val out_gen :
   ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
 
-
 (** [in_generic] is used in combination with camlp4 [Gramext.action] magic
 
    [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
@@ -313,3 +313,5 @@ type an_arg_of_this_type
 
 val in_generic :
   argument_type -> an_arg_of_this_type -> 'co generic_argument
+
+val default_empty_value : ('a,glevel) abstract_argument_type -> 'a option