aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.ml')
-rw-r--r--kernel/term.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index 258f8423c..fa204b570 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -198,7 +198,7 @@ let is_small = function
| Prop _ -> true
| _ -> false
-let iskind c = isprop c or is_Type c
+let iskind c = isprop c || is_Type c
(* Tests if an evar *)
let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false