From 826eb7c6d11007dfd747d49852e71a22e0a3850a Mon Sep 17 00:00:00 2001
From: xclerc
Date: Thu, 19 Sep 2013 12:59:04 +0000
Subject: Get rid of the uses of deprecated OCaml elements (still remaining
 compatible with OCaml 3.12.1).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9a11e47dc3..9d2580ce45 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -282,7 +282,7 @@ let typecheck_inductive env mie =
         | _ -> true
         end ->
 	  (* Predicative set: check that the content is indeed predicative *)
-	  if not (is_type0m_univ lev) & not (is_type0_univ lev) then
+	  if not (is_type0m_univ lev) && not (is_type0_univ lev) then
 	    raise (InductiveError LargeNonPropInductiveNotInType);
 	  Inl (info,full_arity,s), cst
       | Prop _ ->
-- 
cgit v1.2.3