aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/argextend.ml4
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-18 18:04:14 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-21 19:36:38 +0100
commit5835804bd69a193b9ea29b6d4c8d0cc03530ccdd (patch)
tree845364c9df4b4db813f910a66487533c12993ca9 /grammar/argextend.ml4
parent9b02ddf179b375cb09966b70dd3b119eda0d92c1 (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.ml42
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$ >>