aboutsummaryrefslogtreecommitdiff
path: root/parsing/q_coqast.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/q_coqast.ml4')
-rw-r--r--parsing/q_coqast.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 2cc30f5edd..7475754c3b 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -182,7 +182,6 @@ let rec mlexpr_of_argtype loc = function
| Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
| Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
| Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
- | Genarg.TacticArgType n -> <:expr< Genarg.TacticArgType $mlexpr_of_int n$ >>
| Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
| Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
| Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>