1 files changed, 29 insertions, 13 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml
index e564bd11..594e8fd9 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -63,23 +63,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
@@ -259,3 +246,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