From 1e5e934a8ce31c129368e57b61e485e6b989c3f4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 Dec 2013 09:55:04 +0100
Subject: Silence compilation warning by avoiding some deprecated constructs.

---
 plugins/micromega/sos.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index eb3d81901c..35699f2193 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -1235,7 +1235,7 @@ let REAL_NONLINEAR_SUBST_PROVER =
     match tm with
       Var(_,Tyapp("real",[])) when not (mem tm fvs) -> Int 1,tm
     | Comb(Comb(Const("real_mul",_),c),(Var(_,_) as t))
-         when is_ratconst c & not (mem t fvs)
+         when is_ratconst c && not (mem t fvs)
           -> rat_of_term c,t
     | Comb(Comb(Const("real_add",_),s),t) ->
          (try substitutable_monomial (union (frees t) fvs) s
@@ -1291,10 +1291,10 @@ let REAL_SOSFIELD =
     with Failure _ -> REAL_SOS t
   and is_inv =
     let is_div = is_binop `(/):real->real->real` in
-    fun tm -> (is_div tm or (is_comb tm & rator tm = inv_tm)) &
+    fun tm -> (is_div tm or (is_comb tm && rator tm = inv_tm)) &&
               not(is_ratconst(rand tm)) in
   let BASIC_REAL_FIELD tm =
-    let is_freeinv t = is_inv t & free_in t tm in
+    let is_freeinv t = is_inv t && free_in t tm in
     let itms = setify(map rand (find_terms is_freeinv tm)) in
     let hyps = map (fun t -> SPEC t REAL_MUL_RINV) itms in
     let tm' = itlist (fun th t -> mk_imp(concl th,t)) hyps tm in
-- 
cgit v1.2.3