diff options
author | 2015-12-18 18:04:14 +0100 | |
---|---|---|
committer | 2015-12-21 19:36:38 +0100 | |
commit | 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd (patch) | |
tree | 845364c9df4b4db813f910a66487533c12993ca9 /grammar/argextend.ml4 | |
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 'grammar/argextend.ml4')
-rw-r--r-- | grammar/argextend.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 842f59809..b9336ce33 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -30,11 +30,9 @@ let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function - | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >> | IdentArgType -> <:expr< Constrarg.wit_ident >> | VarArgType -> <:expr< Constrarg.wit_var >> | ConstrArgType -> <:expr< Constrarg.wit_constr >> - | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >> | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >> | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> |