diff options
| author | Pierre-Marie Pédrot | 2015-12-18 18:04:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-21 19:36:38 +0100 |
| commit | 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd (patch) | |
| tree | 845364c9df4b4db813f910a66487533c12993ca9 /interp/stdarg.ml | |
| parent | 9b02ddf179b375cb09966b70dd3b119eda0d92c1 (diff) | |
Removing ad-hoc interpretation rules for tactic notations and their genarg.
Now that types can share the same dynamic representation, we do not have
to transtype the topelvel values dynamically and just take advantage of
the standard interpretation function.
Diffstat (limited to 'interp/stdarg.ml')
| -rw-r--r-- | interp/stdarg.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 5cfe3854a9..e155a5217d 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -15,9 +15,7 @@ let wit_bool : bool uniform_genarg_type = make0 None "bool" let wit_int : int uniform_genarg_type = - make0 ~dyn:(val_tag (Obj.magic IntOrVarArgType)) None "int" -(** FIXME: IntOrVarArgType is hardwired, but that definition should be the other - way around. *) + make0 None "int" let wit_string : string uniform_genarg_type = make0 None "string" |