diff options
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 620cbf5805..5a583bcb13 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -26,7 +26,7 @@ open Typeops type inductive_error = | NonPos of env * constr * constr | NotEnoughArgs of env * constr * constr - | NotConstructor of env * constr * constr + | NotConstructor of env * identifier * constr * constr * int * int | NonPar of env * constr * int * constr * constr | SameNamesTypes of identifier | SameNamesConstructors of identifier |