Removing the default value mechanism for generic arguments.

There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.

1 files changed, 5 insertions, 5 deletions

diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 9c3ed94130..56b995e537 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -9,19 +9,19 @@
 open Genarg
 
 let wit_unit : unit uniform_genarg_type =
-  make0 None "unit"
+  make0 "unit"
 
 let wit_bool : bool uniform_genarg_type =
-  make0 None "bool"
+  make0 "bool"
 
 let wit_int : int uniform_genarg_type =
-  make0 None "int"
+  make0 "int"
 
 let wit_string : string uniform_genarg_type =
-  make0 None "string"
+  make0 "string"
 
 let wit_pre_ident : string uniform_genarg_type =
-  make0 None "preident"
+  make0 "preident"
 
 let () = register_name0 wit_unit "Stdarg.wit_unit"
 let () = register_name0 wit_bool "Stdarg.wit_bool"