diff options
Diffstat (limited to 'interp/genarg.ml')
| -rw-r--r-- | interp/genarg.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index 294678d48..e5713a6e2 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -33,7 +33,6 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | TacticArgType of int | OpenConstrArgType of bool | ConstrWithBindingsArgType | BindingsArgType @@ -145,10 +144,6 @@ let rawwit_constr_may_eval = ConstrMayEvalArgType let globwit_constr_may_eval = ConstrMayEvalArgType let wit_constr_may_eval = ConstrMayEvalArgType -let rawwit_tactic n = TacticArgType n -let globwit_tactic n = TacticArgType n -let wit_tactic n = TacticArgType n - let rawwit_open_constr_gen b = OpenConstrArgType b let globwit_open_constr_gen b = OpenConstrArgType b let wit_open_constr_gen b = OpenConstrArgType b |