diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-18 18:04:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-21 19:36:38 +0100 |
| commit | 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd (patch) | |
| tree | 845364c9df4b4db813f910a66487533c12993ca9 /lib/genarg.mli | |
| 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 'lib/genarg.mli')
| -rw-r--r-- | lib/genarg.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli index 89ea49ddb..83ba1dd04 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -201,12 +201,10 @@ val pair_val : (Val.t * Val.t) Val.tag type argument_type = (** Basic types *) - | IntOrVarArgType | IdentArgType | VarArgType (** Specific types *) | ConstrArgType - | ConstrMayEvalArgType | OpenConstrArgType | ListArgType of argument_type | OptArgType of argument_type |