aboutsummaryrefslogtreecommitdiff
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/argextend.ml41
-rw-r--r--grammar/q_coqast.ml41
2 files changed, 0 insertions, 2 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 87a0dfa984..f6c223b741 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -33,7 +33,6 @@ let rec make_wit loc = function
| IdentArgType -> <:expr< Constrarg.wit_ident >>
| VarArgType -> <:expr< Constrarg.wit_var >>
| ConstrArgType -> <:expr< Constrarg.wit_constr >>
- | 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$ >>
| PairArgType (t1,t2) ->
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index fc08f0a492..494ec6ba29 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -225,7 +225,6 @@ let mlexpr_of_red_expr = function
let rec mlexpr_of_argtype loc = function
| Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
| Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
- | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
| Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
| Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
| Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>