diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 09:55:04 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 09:55:04 +0100 |
| commit | 1e5e934a8ce31c129368e57b61e485e6b989c3f4 (patch) | |
| tree | 5ea4ce12c4faf03b631f452e4a362eb40bc422b5 | |
| parent | 24d17c1084d0926047b7ce5c7e3adac43f62378a (diff) | |
Silence compilation warning by avoiding some deprecated constructs.
| -rw-r--r-- | ide/nanoPG.ml | 2 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 2 | ||||
| -rw-r--r-- | plugins/micromega/sos.ml | 6 |
3 files changed, 5 insertions, 5 deletions
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index dafb0575d..fe9e815c9 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -64,7 +64,7 @@ let make_emacs_mode gui name enter_sym bindings = let compile_emacs_modes gui l = List.fold_left (fun (r,s,u,m,d) mode -> let run, set, unset, mask,doc = mode gui in - (fun k -> r k || run k), (fun k -> s k or set k), + (fun k -> r k || run k), (fun k -> s k || set k), (fun () -> u (); unset ()), (fun k -> m k || mask k), d^"\n"^doc) ((fun _ -> false),(fun _ -> false),(fun () -> ()),(fun _ -> false),"") l diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 7317f1abc..43564ba57 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -60,7 +60,7 @@ let is_substring s1 s2 = let i = ref 0 in let len1 = Array.length s1 in let len2 = Array.length s2 in - while !break && !i < len1 & !i < len2 do + while !break && !i < len1 && !i < len2 do break := s1.(!i) = s2.(!i); incr i; done; diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index eb3d81901..35699f219 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 |