aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/heads.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/heads.ml')
-rw-r--r--library/heads.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/heads.ml b/library/heads.ml
index 0d3ed0fdb..62e27dd00 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -92,7 +92,7 @@ let kind_of_head env t =
| [] ->
let () = assert (not b) in
aux (k + 1) [] c b
- | h :: l -> aux (k + 1) l (subst1 h c) b
+ | h :: l -> aux k l (subst1 h c) b
end
| LetIn _ -> assert false
| Meta _ | Evar _ -> NotImmediatelyComputableHead