diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 1a51ea4db7..35a7036af4 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -108,9 +108,9 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys = raise_type_error ?loc (env, sigma, IllTypedRecBody (i, na, jl, tys)) -let error_elim_arity ?loc env sigma pi s c j a = +let error_elim_arity ?loc env sigma pi c j a = raise_type_error ?loc - (env, sigma, ElimArity (pi, s, c, j, a)) + (env, sigma, ElimArity (pi, c, j, a)) let error_not_a_type ?loc env sigma j = raise_type_error ?loc (env, sigma, NotAType j) |