diff options
Diffstat (limited to 'parsing/argextend.ml4')
| -rw-r--r-- | parsing/argextend.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index df48f5d8de..78128a99d8 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -33,7 +33,7 @@ let rec make_rawwit loc = function | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> | TacticArgType -> <:expr< Genarg.rawwit_tactic >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> @@ -59,7 +59,7 @@ let rec make_globwit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.globwit_tactic >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.globwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> @@ -85,7 +85,7 @@ let rec make_wit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.wit_tactic >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.wit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> |