diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-03 16:28:20 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:45:19 +0200 |
| commit | 47e010c2dd0ab6370704d8ab24552753e4e1b1dc (patch) | |
| tree | 27a313f6e00a36aea501c1483f5550f2b9b1229e /kernel/indtypes.ml | |
| parent | f27f3ca3a39f5320a60c82c601525e7f0fe666cb (diff) | |
Fix typo in error message
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 068332406..91e6ec285 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -217,7 +217,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter try basic_check env typ'; Environ.push_rel typ typ_env with NotConvertible -> - anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation!") + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") end | _ -> anomaly (Pp.str "") in |