aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/type_errors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/type_errors.ml')
-rw-r--r--checker/type_errors.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index 9a4d06d78..2963b3ba3 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -20,7 +20,7 @@ type guard_error =
(* Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of constr
- | RecursionOnIllegalTerm of int * constr * int list * int list
+ | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(* CoFixpoints *)
| CodomainNotInductiveType of constr