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