aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/type_errors.mli')
-rw-r--r--kernel/type_errors.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index b194dac97..b4897d612 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -34,7 +34,7 @@ type guard_error =
| RecCallInCaseFun of constr
| RecCallInCaseArg of constr
| RecCallInCasePred of constr
- | NotGuardedForm
+ | NotGuardedForm of constr
type arity_error =
| NonInformativeToInformative