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 2a42888d5..c52a5eb23 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -109,7 +109,7 @@ let kind_of_head env t =
(* enough arguments to [cst] *)
k,List.skipn n l,List.nth l (i-1) in
let l' = List.make q (mkMeta 0) @ rest in
- aux k' l' a (with_subcase or with_case)
+ aux k' l' a (with_subcase || with_case)
| ConstructorHead when with_case -> NotImmediatelyComputableHead
| x -> x
in aux 0 [] t false