Merge branch 'trunk' into located_switch

4 files changed, 53 insertions, 291 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 79d17db25..b6ad784d9 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -331,7 +331,6 @@ module M =
 struct
 
   open Coqlib
-  open Term
   open Constr
   open EConstr
 
@@ -901,16 +900,13 @@ struct
    coq_Qeq, Mc.OpEq
   ]
 
-  let has_typ gl t1 typ = 
-   let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in
-   EConstr.eq_constr (Tacmach.project gl) ty typ
-
+  type gl = { env : Environ.env; sigma : Evd.evar_map }
 
   let is_convertible gl t1 t2 = 
-   Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
+   Reductionops.is_conv gl.env gl.sigma t1 t2
 
   let parse_zop gl (op,args) =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
     match EConstr.kind sigma op with
     | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
     | Ind((n,0),_) ->
@@ -920,7 +916,7 @@ struct
     |   _ -> failwith "parse_zop"
 
   let parse_rop gl (op,args) =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
     match EConstr.kind sigma op with
      | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
      | Ind((n,0),_) ->
@@ -930,7 +926,7 @@ struct
     |   _ -> failwith "parse_zop"
 
   let parse_qop gl (op,args) =
-    (assoc_const (Tacmach.project gl) op qop_table, args.(0) , args.(1))
+    (assoc_const gl.sigma op qop_table, args.(0) , args.(1))
 
   let is_constant sigma t = (* This is an approx *)
    match EConstr.kind sigma t with
@@ -1154,7 +1150,7 @@ struct
    rop_spec
 
   let  parse_arith parse_op parse_expr env cstr gl =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
    if debug
    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
    match EConstr.kind sigma cstr with
@@ -1199,7 +1195,7 @@ struct
     *)
   
   let parse_formula gl parse_atom env tg term =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
 
     let parse_atom env tg t =
       try
@@ -1208,7 +1204,7 @@ struct
       with e when CErrors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
-      let sort  = Retyping.get_sort_of (Tacmach.pf_env gl)  (Tacmach.project gl) term in 
+      let sort  = Retyping.get_sort_of gl.env gl.sigma term in 
      Sorts.is_prop sort in
      
     let rec xparse_formula env tg term =
@@ -1720,7 +1716,6 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let vm = dump_varmap (spec.typ) (vm_of_list env) in
  (* todo : directly generate the proof term - or generalize before conversion? *)
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-   let gl = Tacmach.New.of_old (fun x -> x) gl in
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1730,7 +1725,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
        ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
        ("__wit", cert, cert_typ)
       ]
-      (Tacmach.pf_concl gl))
+      (Tacmach.New.pf_concl gl))
   ] 
   end }
 
@@ -1967,11 +1962,13 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
     Some (ids,ff',res')
 
 
-
 (**
   * Parse the proof environment, and call micromega_tauto
   *)
 
+let fresh_id avoid id gl =
+  Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
 let micromega_gen
     parse_arith 
     (negate:'cst atom -> 'cst mc_cnf)
@@ -1979,17 +1976,17 @@ let micromega_gen
     unsat deduce 
     spec dumpexpr prover tac =
  Proofview.Goal.nf_enter { enter = begin fun gl -> 
-    let gl = Tacmach.New.of_old (fun x -> x) gl in
-    let sigma = Tacmach.project gl in
-    let concl = Tacmach.pf_concl gl in
-    let hyps  = Tacmach.pf_hyps_types gl in
+    let sigma = Tacmach.New.project gl in
+    let concl = Tacmach.New.pf_concl gl in
+    let hyps  = Tacmach.New.pf_hyps_types gl in
     try
-     let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+     let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+     let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
      let env = Env.elements env in
      let spec = Lazy.force spec in
      let dumpexpr = Lazy.force dumpexpr in
      
-     match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl with
+     match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl0 with
      | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
      | Some (ids,ff',res') -> 
        let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in
@@ -1998,7 +1995,7 @@ let micromega_gen
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
 
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
@@ -2057,7 +2054,6 @@ let micromega_order_changer cert env ff  =
   let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
   let vm = dump_varmap (typ) (vm_of_list env) in
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-    let gl = Tacmach.New.of_old (fun x -> x) gl in
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -2069,7 +2065,7 @@ let micromega_order_changer cert env ff  =
 	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|]));
          ("__wit", cert, cert_typ)
         ]
-        (Tacmach.pf_concl gl)));
+        (Tacmach.New.pf_concl gl)));
      (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
      ]
   end }
@@ -2088,20 +2084,20 @@ let micromega_genr prover tac =
     dump_proof = dump_psatz coq_Q dump_q
   } in
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-     let gl = Tacmach.New.of_old (fun x -> x) gl in
-     let sigma = Tacmach.project gl in
-     let concl = Tacmach.pf_concl gl in
-     let hyps  = Tacmach.pf_hyps_types gl in
+     let sigma = Tacmach.New.project gl in
+     let concl = Tacmach.New.pf_concl gl in
+     let hyps  = Tacmach.New.pf_hyps_types gl in
 
      try
-      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+      let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+      let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
        let env = Env.elements env in
        let spec = Lazy.force spec in
        
        let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
        let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
        
-       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl with
+       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl0 with
        | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") 
        | Some (ids,ff',res') -> 
          let (ff,ids) = formula_hyps_concl 
@@ -2114,7 +2110,7 @@ let micromega_genr prover tac =
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
        
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index f4f9b3c2f..377994415 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -99,7 +99,7 @@ module PSet = ISet
 module System = Hashtbl.Make(Vect)
 
 type proof =
-| Hyp of int
+| Assum of int
 | Elim of  var * proof * proof
 | And of proof * proof
 
@@ -134,7 +134,7 @@ exception SystemContradiction of proof
 let hyps prf =
   let rec hyps prf acc =
     match prf with
-      | Hyp i -> ISet.add i acc
+      | Assum i -> ISet.add i acc
       | Elim(_,prf1,prf2)
       | And(prf1,prf2) -> hyps prf1 (hyps prf2 acc) in
     hyps prf ISet.empty
@@ -143,7 +143,7 @@ let hyps prf =
 (** Pretty printing *)
   let rec pp_proof o prf =
     match prf with
-      | Hyp i -> Printf.fprintf o "H%i" i
+      | Assum i -> Printf.fprintf o "H%i" i
       | Elim(v, prf1,prf2) -> Printf.fprintf o "E(%i,%a,%a)" v pp_proof prf1 pp_proof prf2
       | And(prf1,prf2)   -> Printf.fprintf o "A(%a,%a)"  pp_proof prf1 pp_proof prf2
 
@@ -270,7 +270,7 @@ let norm_cstr {coeffs = v ; op = o ; cst = c} idx =
   (match o with
 	| Eq -> Some c , Some c
 	| Ge -> Some c , None) ;
-	    prf = Hyp idx }
+	    prf = Assum idx }
 
 
 (** [load_system l] takes a list of constraints of type [cstr_compat]
@@ -285,7 +285,7 @@ let load_system l =
 
   let vars = List.fold_left (fun vrs (cstr,i) ->
     match norm_cstr cstr i with
-      | Contradiction -> raise (SystemContradiction (Hyp i))
+      | Contradiction -> raise (SystemContradiction (Assum i))
       | Redundant      -> vrs
       | Cstr(vect,info) ->
 	  xadd_cstr  vect info sys ;
@@ -867,7 +867,7 @@ let  mk_proof hyps prf =
 
   let rec mk_proof prf =
     match prf with
-      | Hyp i -> [ ([i, Int 1] , List.nth hyps i) ]
+      | Assum i -> [ ([i, Int 1] , List.nth hyps i) ]
 
       | Elim(v,prf1,prf2) ->
           let prfsl = mk_proof prf1
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index cc89e2b9d..e1ceabe9e 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -21,8 +21,6 @@ let debugging = ref false;;
 
 exception Sanity;;
 
-exception Unsolvable;;
-
 (* ------------------------------------------------------------------------- *)
 (* Turn a rational into a decimal string with d sig digits.                  *)
 (* ------------------------------------------------------------------------- *)
@@ -99,28 +97,11 @@ let vector_const c n =
   if c =/ Int 0 then vector_0 n
   else (n,itlist (fun k -> k |-> c) (1--n) undefined :vector);;
 
-let vector_1 = vector_const (Int 1);;
-
 let vector_cmul c (v:vector) =
   let n = dim v in
   if c =/ Int 0 then vector_0 n
   else n,mapf (fun x -> c */ x) (snd v)
 
-let vector_neg (v:vector) = (fst v,mapf minus_num (snd v) :vector);;
-
-let vector_add (v1:vector) (v2:vector) =
-  let m = dim v1 and n = dim v2 in
-  if m <> n then failwith "vector_add: incompatible dimensions" else
-  (n,combine (+/) (fun x -> x =/ Int 0) (snd v1) (snd v2) :vector);;
-
-let vector_sub v1 v2 = vector_add v1 (vector_neg v2);;
-
-let vector_dot (v1:vector) (v2:vector) =
-  let m = dim v1 and n = dim v2 in
-  if m <> n then failwith "vector_add: incompatible dimensions" else
-  foldl (fun a i x -> x +/ a) (Int 0)
-        (combine ( */ ) (fun x -> x =/ Int 0) (snd v1) (snd v2));;
-
 let vector_of_list l =
   let n = List.length l in
   (n,itlist2 (|->) (1--n) l undefined :vector);;
@@ -133,13 +114,6 @@ let matrix_0 (m,n) = ((m,n),undefined:matrix);;
 
 let dimensions (m:matrix) = fst m;;
 
-let matrix_const c (m,n as mn) =
-  if m <> n then failwith "matrix_const: needs to be square"
-  else if c =/ Int 0 then matrix_0 mn
-  else (mn,itlist (fun k -> (k,k) |-> c) (1--n) undefined :matrix);;
-
-let matrix_1 = matrix_const (Int 1);;
-
 let matrix_cmul c (m:matrix) =
   let (i,j) = dimensions m in
   if c =/ Int 0 then matrix_0 (i,j)
@@ -152,8 +126,6 @@ let matrix_add (m1:matrix) (m2:matrix) =
   if d1 <> d2 then failwith "matrix_add: incompatible dimensions"
   else (d1,combine (+/) (fun x -> x =/ Int 0) (snd m1) (snd m2) :matrix);;
 
-let matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);;
-
 let row k (m:matrix) =
   let i,j = dimensions m in
   (j,
@@ -166,20 +138,10 @@ let column k (m:matrix) =
    foldl (fun a (i,j) c -> if j = k then (i |-> c) a else a) undefined (snd m)
    : vector);;
 
-let transp (m:matrix) =
-  let i,j = dimensions m in
-  ((j,i),foldl (fun a (i,j) c -> ((j,i) |-> c) a) undefined (snd m) :matrix);;
-
 let diagonal (v:vector) =
   let n = dim v in
   ((n,n),foldl (fun a i c -> ((i,i) |-> c) a) undefined (snd v) : matrix);;
 
-let matrix_of_list l =
-  let m = List.length l in
-  if m = 0 then matrix_0 (0,0) else
-  let n = List.length (List.hd l) in
-  (m,n),itern 1 l (fun v i -> itern 1 v (fun c j -> (i,j) |-> c)) undefined;;
-
 (* ------------------------------------------------------------------------- *)
 (* Monomials.                                                                *)
 (* ------------------------------------------------------------------------- *)
@@ -195,24 +157,8 @@ let monomial_var x = (x |=> 1 :monomial);;
 let (monomial_mul:monomial->monomial->monomial) =
   combine (+) (fun x -> false);;
 
-let monomial_pow (m:monomial) k =
-  if k = 0 then monomial_1
-  else mapf (fun x -> k * x) m;;
-
-let monomial_divides (m1:monomial) (m2:monomial) =
-  foldl (fun a x k -> tryapplyd m2 x 0 >= k && a) true m1;;
-
-let monomial_div (m1:monomial) (m2:monomial) =
-  let m = combine (+) (fun x -> x = 0) m1 (mapf (fun x -> -x) m2) in
-  if foldl (fun a x k -> k >= 0 && a) true m then m
-  else failwith "monomial_div: non-divisible";;
-
 let monomial_degree x (m:monomial) = tryapplyd m x 0;;
 
-let monomial_lcm (m1:monomial) (m2:monomial) =
-  (itlist (fun x -> x |-> max (monomial_degree x m1) (monomial_degree x m2))
-          (union (dom m1) (dom m2)) undefined :monomial);;
-
 let monomial_multidegree (m:monomial) = foldl (fun a x k -> k + a) 0 m;;
 
 let monomial_variables m = dom m;;
@@ -252,12 +198,6 @@ let poly_cmmul (c,m) (p:poly) =
 let poly_mul (p1:poly) (p2:poly) =
   foldl (fun a m c -> poly_add (poly_cmmul (c,m) p2) a) poly_0 p1;;
 
-let poly_div (p1:poly) (p2:poly) =
-  if not(poly_isconst p2) then failwith "poly_div: non-constant" else
-  let c = eval undefined p2 in
-  if c =/ Int 0 then failwith "poly_div: division by zero"
-  else poly_cmul (Int 1 // c) p1;;
-
 let poly_square p = poly_mul p p;;
 
 let rec poly_pow p k =
@@ -266,10 +206,6 @@ let rec poly_pow p k =
   else let q = poly_square(poly_pow p (k / 2)) in
        if k mod 2 = 1 then poly_mul p q else q;;
 
-let poly_exp p1 p2 =
-  if not(poly_isconst p2) then failwith "poly_exp: not a constant" else
-  poly_pow p1 (Num.int_of_num (eval undefined p2));;
-
 let degree x (p:poly) = foldl (fun a m c -> max (monomial_degree x m) a) 0 p;;
 
 let multidegree (p:poly) =
@@ -282,14 +218,14 @@ let poly_variables (p:poly) =
 (* Order monomials for human presentation.                                   *)
 (* ------------------------------------------------------------------------- *)
 
-let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 or x1 = x2 && k1 > k2;;
+let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 || x1 = x2 && k1 > k2;;
 
 let humanorder_monomial =
   let rec ord l1 l2 = match (l1,l2) with
     _,[] -> true
   | [],_ -> false
-  | h1::t1,h2::t2 -> humanorder_varpow h1 h2 or h1 = h2 && ord t1 t2 in
-  fun m1 m2 -> m1 = m2 or
+  | h1::t1,h2::t2 -> humanorder_varpow h1 h2 || h1 = h2 && ord t1 t2 in
+  fun m1 m2 -> m1 = m2 ||
                ord (sort humanorder_varpow (graph m1))
                    (sort humanorder_varpow (graph m2));;
 
@@ -297,42 +233,8 @@ let humanorder_monomial =
 (* Conversions to strings.                                                   *)
 (* ------------------------------------------------------------------------- *)
 
-let string_of_vector min_size max_size (v:vector) =
-  let n_raw = dim v in
-  if n_raw = 0 then "[]" else
-  let n = max min_size (min n_raw max_size) in
-  let xs = List.map ((o) string_of_num (element v)) (1--n) in
-  "[" ^ end_itlist (fun s t -> s ^ ", " ^ t) xs ^
-  (if n_raw > max_size then ", ...]" else "]");;
-
-let string_of_matrix max_size (m:matrix) =
-  let i_raw,j_raw = dimensions m in
-  let i = min max_size i_raw and j = min max_size j_raw in
-  let rstr = List.map (fun k -> string_of_vector j j (row k m)) (1--i) in
-  "["^end_itlist(fun s t -> s^";\n "^t) rstr ^
-  (if j > max_size then "\n ...]" else "]");;
-
 let string_of_vname (v:vname): string = (v: string);;
 
-let rec string_of_term t =
-  match t with
-  Opp t1 -> "(- " ^ string_of_term t1 ^ ")"
-| Add (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " + " ^ (string_of_term t2) ^ ")"
-| Sub (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " - " ^ (string_of_term t2) ^ ")"
-| Mul (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " * " ^ (string_of_term t2) ^ ")"
-| Inv t1 -> "(/ " ^ string_of_term t1 ^ ")"
-| Div (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " / " ^ (string_of_term t2) ^ ")"
-| Pow (t1, n1) ->
-   "(" ^ (string_of_term t1) ^ " ^ " ^ (string_of_int n1) ^ ")"
-| Zero -> "0"
-| Var v -> "x" ^ (string_of_vname v)
-| Const x -> string_of_num x;;
-
-
 let string_of_varpow x k =
   if k = 1 then string_of_vname x else string_of_vname x^"^"^string_of_int k;;
 
@@ -363,6 +265,7 @@ let string_of_poly (p:poly) =
 (* Printers.                                                                 *)
 (* ------------------------------------------------------------------------- *)
 
+(*
 let print_vector v = Format.print_string(string_of_vector 0 20 v);;
 
 let print_matrix m = Format.print_string(string_of_matrix 20 m);;
@@ -371,7 +274,6 @@ let print_monomial m = Format.print_string(string_of_monomial m);;
 
 let print_poly m = Format.print_string(string_of_poly m);;
 
-(*
 #install_printer print_vector;;
 #install_printer print_matrix;;
 #install_printer print_monomial;;
@@ -411,19 +313,6 @@ let sdpa_of_vector (v:vector) =
   end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";;
 
 (* ------------------------------------------------------------------------- *)
-(* String for block diagonal matrix numbered k.                              *)
-(* ------------------------------------------------------------------------- *)
-
-let sdpa_of_blockdiagonal k m =
-  let pfx = string_of_int k ^" " in
-  let ents =
-    foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in
-  let entss = sort (increasing fst) ents in
-  itlist (fun ((b,i,j),c) a ->
-     pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
-     " " ^ decimalize 20 c ^ "\n" ^ a) entss "";;
-
-(* ------------------------------------------------------------------------- *)
 (* String for a matrix numbered k, in SDPA sparse format.                    *)
 (* ------------------------------------------------------------------------- *)
 
@@ -466,6 +355,7 @@ let token s =
   >> (fun ((_,t),_) -> t);;
 
 let decimal =
+  let (||) = parser_or in
   let numeral = some isnum in
   let decimalint = atleast 1 numeral >> ((o) Num.num_of_string  implode) in
   let decimalfrac = atleast 1 numeral
@@ -485,13 +375,12 @@ let mkparser p s =
   let x,rst = p(explode s) in
   if rst = [] then x else failwith "mkparser: unparsed input";;
 
-let parse_decimal = mkparser decimal;;
-
 (* ------------------------------------------------------------------------- *)
 (* Parse back a vector.                                                      *)
 (* ------------------------------------------------------------------------- *)
 
-let parse_sdpaoutput,parse_csdpoutput =
+let _parse_sdpaoutput, parse_csdpoutput =
+  let (||) = parser_or in
   let vector =
     token "{" ++ listof decimal (token ",") "decimal" ++ token "}"
                >> (fun ((_,v),_) -> vector_of_list v) in
@@ -508,23 +397,10 @@ let parse_sdpaoutput,parse_csdpoutput =
   mkparser sdpaoutput,mkparser csdpoutput;;
 
 (* ------------------------------------------------------------------------- *)
-(* Also parse the SDPA output to test success (CSDP yields a return code).   *)
-(* ------------------------------------------------------------------------- *)
-
-let sdpa_run_succeeded =
-   let rec skipupto dscr prs inp =
-      (dscr ++ prs >> snd
-    || some (fun c -> true) ++ skipupto dscr prs >> snd) inp in
-  let prs = skipupto (word "phase.value" ++ token "=")
-                     (possibly (a "p") ++ possibly (a "d") ++
-                      (word "OPT" || word "FEAS")) in
-  fun s -> try ignore (prs (explode s)); true with Noparse -> false;;
-
-(* ------------------------------------------------------------------------- *)
 (* The default parameters. Unfortunately this goes to a fixed file.          *)
 (* ------------------------------------------------------------------------- *)
 
-let sdpa_default_parameters =
+let _sdpa_default_parameters =
 "100     unsigned int maxIteration;\
 \n1.0E-7  double 0.0 < epsilonStar;\
 \n1.0E2   double 0.0 < lambdaStar;\
@@ -555,7 +431,7 @@ let sdpa_alt_parameters =
 \n1.0E-7  double 0.0 < epsilonDash;\
 \n";;
 
-let sdpa_params = sdpa_alt_parameters;;
+let _sdpa_params = sdpa_alt_parameters;;
 
 (* ------------------------------------------------------------------------- *)
 (* CSDP parameters; so far I'm sticking with the defaults.                   *)
@@ -588,10 +464,10 @@ let run_csdp dbg obj mats =
   let input_file = Filename.temp_file "sos" ".dat-s" in
   let output_file =
     String.sub input_file 0 (String.length input_file - 6) ^ ".out"
-  and params_file = Filename.concat (!temp_path) "param.csdp" in
+  and params_file = Filename.concat temp_path "param.csdp" in
   file_of_string input_file (sdpa_of_problem "" obj mats);
   file_of_string params_file csdp_params;
-  let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^
+  let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^
                         " " ^ output_file ^
                        (if dbg then "" else "> /dev/null")) in
   let op = string_of_file output_file in
@@ -600,16 +476,6 @@ let run_csdp dbg obj mats =
     else (Sys.remove input_file; Sys.remove output_file));
     rv,res);;
 
-let csdp obj mats =
-  let rv,res = run_csdp (!debugging) obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
-   else if rv = 3 then ()
-    (* Format.print_string "csdp warning: Reduced accuracy";
-     Format.print_newline() *)
-   else if rv <> 0 then failwith("csdp: error "^string_of_int rv)
-   else ());
-  res;;
-
 (* ------------------------------------------------------------------------- *)
 (* Try some apparently sensible scaling first. Note that this is purely to   *)
 (* get a cleaner translation to floating-point, and doesn't affect any of    *)
@@ -653,21 +519,7 @@ let linear_program_basic a =
   let mats =  List.map (fun j -> diagonal (column j a)) (1--n)
   and obj = vector_const (Int 1) m in
   let rv,res = run_csdp false obj mats in
-  if rv = 1 or rv = 2 then false
-  else if rv = 0 then true
-  else failwith "linear_program: An error occurred in the SDP solver";;
-
-(* ------------------------------------------------------------------------- *)
-(* Alternative interface testing A x >= b for matrix A, vector b.            *)
-(* ------------------------------------------------------------------------- *)
-
-let linear_program a b =
-  let m,n = dimensions a in
-  if dim b <> m then failwith "linear_program: incompatible dimensions" else
-  let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n)
-  and obj = vector_const (Int 1) m in
-  let rv,res = run_csdp false obj mats in
-  if rv = 1 or rv = 2 then false
+  if rv = 1 || rv = 2 then false
   else if rv = 0 then true
   else failwith "linear_program: An error occurred in the SDP solver";;
 
@@ -716,40 +568,6 @@ let equation_eval assig eq =
   foldl (fun a v c -> a +/ value(v) */ c) (Int 0) eq;;
 
 (* ------------------------------------------------------------------------- *)
-(* Eliminate among linear equations: return unconstrained variables and      *)
-(* assignments for the others in terms of them. We give one pseudo-variable  *)
-(* "one" that's used for a constant term.                                    *)
-(* ------------------------------------------------------------------------- *)
-
-let failstore = ref [];;
-
-let eliminate_equations =
-  let rec extract_first p l =
-    match l with
-      [] -> failwith "extract_first"
-    | h::t -> if p(h) then h,t else
-              let k,s = extract_first p t in
-              k,h::s in
-  let rec eliminate vars dun eqs =
-    match vars with
-      [] -> if forall is_undefined eqs then dun
-            else (failstore := [vars,dun,eqs]; raise Unsolvable)
-    | v::vs ->
-            try let eq,oeqs = extract_first (fun e -> defined e v) eqs in
-                let a = apply eq v in
-                let eq' = equation_cmul (Int(-1) // a) (undefine v eq) in
-                let elim e =
-                  let b = tryapplyd e v (Int 0) in
-                  if b =/ Int 0 then e else
-                  equation_add e (equation_cmul (minus_num b // a) eq) in
-                eliminate vs ((v |-> eq') (mapf elim dun)) (List.map elim oeqs)
-            with Failure _ -> eliminate vs dun eqs in
-  fun one vars eqs ->
-    let assig = eliminate vars undefined eqs in
-    let vs = foldl (fun a x f -> subtract (dom f) [one] @ a) [] assig in
-    setify vs,assig;;
-
-(* ------------------------------------------------------------------------- *)
 (* Eliminate all variables, in an essentially arbitrary order.               *)
 (* ------------------------------------------------------------------------- *)
 
@@ -780,18 +598,6 @@ let eliminate_all_equations one =
     setify vs,assig;;
 
 (* ------------------------------------------------------------------------- *)
-(* Solve equations by assigning arbitrary numbers.                           *)
-(* ------------------------------------------------------------------------- *)
-
-let solve_equations one eqs =
-  let vars,assigs = eliminate_all_equations one eqs in
-  let vfn = itlist (fun v -> (v |-> Int 0)) vars (one |=> Int(-1)) in
-  let ass =
-    combine (+/) (fun c -> false) (mapf (equation_eval vfn) assigs) vfn in
-  if forall (fun e -> equation_eval ass e =/ Int 0) eqs
-  then undefine one ass else raise Sanity;;
-
-(* ------------------------------------------------------------------------- *)
 (* Hence produce the "relevant" monomials: those whose squares lie in the    *)
 (* Newton polytope of the monomials in the input. (This is enough according  *)
 (* to Reznik: "Extremal PSD forms with few terms", Duke Math. Journal,       *)
@@ -898,19 +704,6 @@ let epoly_pmul p q acc =
                  a q) acc p;;
 
 (* ------------------------------------------------------------------------- *)
-(* Usual operations on equation-parametrized poly.                           *)
-(* ------------------------------------------------------------------------- *)
-
-let epoly_cmul c l =
-  if c =/ Int 0 then undefined else mapf (equation_cmul c) l;;
-
-let epoly_neg = epoly_cmul (Int(-1));;
-
-let epoly_add = combine equation_add is_undefined;;
-
-let epoly_sub p q = epoly_add p (epoly_neg q);;
-
-(* ------------------------------------------------------------------------- *)
 (* Convert regular polynomial. Note that we treat (0,0,0) as -1.             *)
 (* ------------------------------------------------------------------------- *)
 
@@ -953,11 +746,11 @@ let run_csdp dbg nblocks blocksizes obj mats =
   let input_file = Filename.temp_file "sos" ".dat-s" in
   let output_file =
     String.sub input_file 0 (String.length input_file - 6) ^ ".out"
-  and params_file = Filename.concat (!temp_path) "param.csdp" in
+  and params_file = Filename.concat temp_path "param.csdp" in
   file_of_string input_file
    (sdpa_of_blockproblem "" nblocks blocksizes obj mats);
   file_of_string params_file csdp_params;
-  let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^
+  let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^
                         " " ^ output_file ^
                        (if dbg then "" else "> /dev/null")) in
   let op = string_of_file output_file in
@@ -968,7 +761,7 @@ let run_csdp dbg nblocks blocksizes obj mats =
 
 let csdp nblocks blocksizes obj mats =
   let rv,res = run_csdp (!debugging) nblocks blocksizes obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
    else if rv = 3 then ()
     (*Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline() *)
@@ -988,8 +781,6 @@ let bmatrix_cmul c bm =
 
 let bmatrix_neg = bmatrix_cmul (Int(-1));;
 
-let bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
-
 (* ------------------------------------------------------------------------- *)
 (* Smash a block matrix into components.                                     *)
 (* ------------------------------------------------------------------------- *)
@@ -1102,15 +893,6 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
   cfs,List.map (fun (a,b) -> snd a,b) msq;;
 
 (* ------------------------------------------------------------------------- *)
-(* Iterative deepening.                                                      *)
-(* ------------------------------------------------------------------------- *)
-
-let rec deepen f n =
-  try print_string "Searching with depth limit ";
-      print_int n; print_newline(); f n
-  with Failure _ -> deepen f (n + 1);;
-
-(* ------------------------------------------------------------------------- *)
 (* The ordering so we can create canonical HOL polynomials.                  *)
 (* ------------------------------------------------------------------------- *)
 
@@ -1136,10 +918,6 @@ let monomial_order =
     if deg1 < deg2 then false else if deg1 > deg2 then true
     else lexorder mon1 mon2;;
 
-let dest_poly p =
-  List.map (fun (m,c) -> c,dest_monomial m)
-      (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p));;
-
 (* ------------------------------------------------------------------------- *)
 (* Map back polynomials and their composites to HOL.                         *)
 (* ------------------------------------------------------------------------- *)
@@ -1373,9 +1151,6 @@ let rec allpermutations l =
   itlist (fun h acc -> List.map (fun t -> h::t)
                 (allpermutations (subtract l [h])) @ acc) l [];;
 
-let allvarorders l =
-  List.map (fun vlis x -> index x vlis) (allpermutations l);;
-
 let changevariables_monomial zoln (m:monomial) =
   foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;;
 
@@ -1392,15 +1167,6 @@ let sdpa_of_vector (v:vector) =
   let strs = List.map (o (decimalize 20) (element v)) (1--n) in
   end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";;
 
-let sdpa_of_blockdiagonal k m =
-  let pfx = string_of_int k ^" " in
-  let ents =
-    foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in
-  let entss = sort (increasing fst) ents in
-  itlist (fun ((b,i,j),c) a ->
-     pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
-     " " ^ decimalize 20 c ^ "\n" ^ a) entss "";;
-
 let sdpa_of_matrix k (m:matrix) =
   let pfx = string_of_int k ^ " 1 " in
   let ms = foldr (fun (i,j) c a -> if i > j then a else ((i,j),c)::a)
@@ -1425,10 +1191,10 @@ let run_csdp dbg obj mats =
   let input_file = Filename.temp_file "sos" ".dat-s" in
   let output_file =
     String.sub input_file 0 (String.length input_file - 6) ^ ".out"
-  and params_file = Filename.concat (!temp_path) "param.csdp" in
+  and params_file = Filename.concat temp_path "param.csdp" in
   file_of_string input_file (sdpa_of_problem "" obj mats);
   file_of_string params_file csdp_params;
-  let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^
+  let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^
                        " " ^ output_file ^
                        (if dbg then "" else "> /dev/null")) in
   let op = string_of_file output_file in
@@ -1439,7 +1205,7 @@ let run_csdp dbg obj mats =
 
 let csdp obj mats =
   let rv,res = run_csdp (!debugging) obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
     else if rv = 3 then ()
 (*    (Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline()) *)
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index f54914f25..6b8b820ac 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -525,7 +525,7 @@ let isspace,issep,isbra,issymb,isalpha,isnum,isalnum =
   and isalnum c = Array.get ctable (charcode c) >= 16 in
   isspace,issep,isbra,issymb,isalpha,isnum,isalnum;;
 
-let (||) parser1 parser2 input =
+let parser_or parser1 parser2 input =
   try parser1 input
   with Noparse -> parser2 input;;
 
@@ -571,7 +571,7 @@ let finished input =
 
 (* ------------------------------------------------------------------------- *)
 
-let temp_path = ref Filename.temp_dir_name;;
+let temp_path = Filename.get_temp_dir_name ();;
 
 (* ------------------------------------------------------------------------- *)
 (* Convenient conversion between files and (lists of) strings.               *)