From 8cc623262c625bda20e97c75f9ba083ae8e7760d Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Sep 2012 19:13:19 +0000 Subject: As r15801: putting everything from Util.array_* to CArray.*. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/firstorder/formula.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index f4cc397bc..d224f87df 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -95,7 +95,7 @@ let kind_of_formula gl term = let is_trivial= let is_constant c = nb_prod c = mib.mind_nparams in - array_exists is_constant mip.mind_nf_lc in + Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then @@ -144,7 +144,7 @@ let build_atoms gl metagen side cciterm = let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) - array_exists (function []->true|_->false) v + Array.exists (function []->true|_->false) v then trivial:=true; Array.iter f v | Exists(i,l)-> -- cgit v1.2.3