diff options
Diffstat (limited to 'kernel/type_errors.ml')
| -rw-r--r-- | kernel/type_errors.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index b057ff8391..f1eb32b5bc 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -40,7 +40,7 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * constr list * constr * unsafe_judgment + | ElimArity of inductive * types list * constr * unsafe_judgment * (constr * constr * string) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info |