aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_coqast.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/q_coqast.ml4')
-rw-r--r--grammar/q_coqast.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index b405539ec..3e11bf5a8 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -203,7 +203,6 @@ let mlexpr_of_red_expr = function
let rec mlexpr_of_argtype loc = function
| Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
- | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
| Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
| Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
| Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>