diff options
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 809e5a2300..8a1bbd3cb0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1742,10 +1742,10 @@ and interp_atomic ist gl = function | ConstrMayEvalArgType -> VConstr (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x)) - | StringArgType | BoolArgType - | QuantHypArgType | RedExprArgType | TacticArgType -> val_interp ist gl (out_gen globwit_tactic x) + | StringArgType | BoolArgType + | QuantHypArgType | RedExprArgType | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ -> error "This generic type is not supported in alias" |