Merge PR#582: Fix warnings

46 files changed, 62 insertions, 486 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 00b31cccee..7c5efaea3a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -15,13 +15,11 @@ open Declarations
 open Term
 open EConstr
 open Vars
-open Tacmach
 open Tactics
 open Typing
 open Ccalgo
 open Ccproof
 open Pp
-open CErrors
 open Util
 open Proofview.Notations
 
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 5099d847b0..b4bb62be8e 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -8,7 +8,6 @@
 (************************************************************************)
 
 open EConstr
-open Proof_type
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2b12462ad5..322fbcea74 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -657,7 +657,7 @@ let extraction_library is_rec m =
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, extract_structure env mp no_delta true struc) :: l
+    then (mp, extract_structure env mp no_delta ~all:true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ade94e98e3..9900792cac 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -12,7 +12,6 @@ open Term
 open EConstr
 open Vars
 open Termops
-open Tacmach
 open Util
 open Declarations
 open Globnames
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 8ef6a09d0e..b250175354 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -123,7 +123,6 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
-open Pp
 open Genarg
 open Ppconstr
 open Printer
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 62f811546d..5a1e7c26a1 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -10,14 +10,12 @@ open Unify
 open Rules
 open CErrors
 open Util
-open Term
 open EConstr
 open Vars
 open Tacmach.New
 open Tactics
 open Tacticals.New
 open Proofview.Notations
-open Termops
 open Reductionops
 open Formula
 open Sequent
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e0d2c38a73..86a6770070 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open EConstr
 open Vars
 open Tacmach.New
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 80a7ae2c25..fb21730830 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -8,7 +8,6 @@
 
 open Term
 open EConstr
-open Tacmach
 open Names
 open Globnames
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 59b842c825..2d18b66054 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -12,7 +12,6 @@ open CErrors
 open Util
 open Formula
 open Unify
-open Tacmach
 open Globnames
 open Pp
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 18d68f54f9..6ed251f34e 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -6,10 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Formula
-open Tacmach
 open Globnames
 
 module OrderedConstr: Set.OrderedType with type t=Constr.t
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8dae17d69e..55d361e3d2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -19,12 +19,6 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
-let local_assum (na, t) =
-  RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
-  RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
 (* let msgnl = Pp.msgnl *)
 
 (*
@@ -235,12 +229,13 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
   Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
 
 
+exception NoChange
 
 let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
   let nochange ?t' msg  =
     begin
       observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
-      failwith "NoChange";
+      raise NoChange;
     end
   in
   let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in
@@ -542,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	      tclTHEN
 		tac
 		(scan_type new_context new_t')
-	    with Failure "NoChange" ->
+	    with NoChange ->
 	      (* Last thing todo : push the rel in the context and continue *)
 	      scan_type (LocalAssum (x,t_x) :: context) t'
 	  end
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 7ddc84d015..61752aa339 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,5 +1,4 @@
 open Names
-open Term
 
 val prove_princ_for_struct :
   Evd.evar_map ref ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0dccd25d75..b5eacee818 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -8,7 +8,6 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 open Ltac_plugin
 open Util
-open Term
 open Pp
 open Constrexpr
 open Indfun_common
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7b0d7d27d7..848b44a603 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -21,12 +21,9 @@ let get_name avoid ?(default="H") = function
   | Name n -> Name n
 
 let array_get_start a =
-  try
-    Array.init
-      (Array.length a - 1)
-      (fun i -> a.(i))
-  with Invalid_argument "index out of bounds" ->
-    invalid_arg "array_get_start"
+  Array.init
+    (Array.length a - 1)
+    (fun i -> a.(i))
 
 let id_of_name = function
     Name id -> id
@@ -508,7 +505,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
 let decompose_lam_n sigma n =
-  let open EConstr in
   if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ec0a898a..6c0c28905e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Ltac_plugin
-open Tacexpr
 open Declarations
 open CErrors
 open Util
@@ -1026,7 +1025,7 @@ let invfun qhyp f  =
     | Not_found ->  error "No graph found"
     | Option.IsNone  -> error "Cannot use equivalence with graph!"
 
-
+exception NoFunction
 let invfun qhyp f g =
   match f with
     | Some f -> invfun qhyp f g
@@ -1041,23 +1040,23 @@ let invfun qhyp f g =
 		   begin
 		     let f1,_ = decompose_app sigma args.(1) in
 		     try
-		       if not (isConst sigma f1) then failwith "";
+		       if not (isConst sigma f1) then raise NoFunction;
 		       let finfos = find_Function_infos (fst (destConst sigma f1)) in
 		       let f_correct = mkConst(Option.get finfos.correctness_lemma)
 		       and kn = fst finfos.graph_ind
 		       in
 		       functional_inversion kn hid f1 f_correct g
-		     with | Failure "" | Option.IsNone | Not_found ->
+		     with | NoFunction | Option.IsNone | Not_found ->
 		       try
 			 let f2,_ = decompose_app sigma args.(2) in
-			 if not (isConst sigma f2) then failwith "";
+			 if not (isConst sigma f2) then raise NoFunction;
 			 let finfos = find_Function_infos (fst (destConst sigma f2)) in
 			 let f_correct = mkConst(Option.get finfos.correctness_lemma)
 			 and kn = fst finfos.graph_ind
 			 in
 			 functional_inversion kn hid  f2 f_correct g
 		       with
-			 | Failure "" ->
+			 | NoFunction ->
 			     user_err  (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
 			 | Option.IsNone  ->
 			     if do_observe ()
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f1ca575856..0af0898a0a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
 open Names
 open Term
 open Vars
-open Termops
 open Declarations
 open Glob_term
 open Glob_termops
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1e405d2c90..bd30f11596 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1225,6 +1225,7 @@ let get_current_subgoals_types () =
   let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
     sigma, List.map (Goal.V82.abstract_type sigma) sgs
 
+exception EmptySubgoals
 let build_and_l sigma l =
   let and_constr =  Coqlib.build_coq_and () in
   let conj_constr = coq_conj () in
@@ -1246,7 +1247,7 @@ let build_and_l sigma l =
   in
   let l = List.sort compare l in 
   let rec f  = function
-    | [] -> failwith "empty list of subgoals!"
+    | [] -> raise EmptySubgoals
     | [p] -> p,tclIDTAC,1
     | p1::pl ->
 	let c,tac,nb = f pl in
@@ -1432,7 +1433,7 @@ let com_terminate
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type);
-  with Failure "empty list of subgoals!" ->
+  with EmptySubgoals ->
     (* a non recursive function declared with measure ! *)
     tcc_lemma_ref := Not_needed;
     defined ()
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 5d3f6df03d..bc9c300e23 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -9,7 +9,6 @@
 open Util
 open Names
 open Term
-open EConstr
 open CErrors
 open Evar_refiner
 open Tacmach
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..21419d1f92 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -21,7 +21,6 @@ open Tacexpr
 open Glob_ops
 open CErrors
 open Util
-open Evd
 open Termops
 open Equality
 open Misctypes
@@ -52,8 +51,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
-let clause = Pltac.clause_dft_concl
-
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfa8331ff2..50e8255a67 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,7 +16,6 @@ open Pcoq.Constr
 open Pltac
 open Hints
 open Tacexpr
-open Proofview.Notations
 open Names
 
 DECLARE PLUGIN "g_auto"
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index ff5e7d5ff2..23ce368eea 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,9 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Misctypes
 open Class_tactics
-open Pltac
 open Stdarg
 open Tacarg
 open Names
@@ -95,7 +93,6 @@ END
 (** TODO: DEPRECATE *)
 (* A progress test that allows to see if the evars have changed *)
 open Term
-open Proofview.Goal
 open Proofview.Notations
 
 let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fdcaedab3a..ac979bcf89 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,6 @@ open Glob_term
 open Geninterp
 open Extraargs
 open Tacmach
-open Tacticals
 open Proofview.Notations
 open Rewrite
 open Stdarg
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae8..7e979d269d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Pcoq
 
 (* Main entry for extensions *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 39ae1f41d2..b73b66e56f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -250,7 +250,7 @@ type 'a extra_genarg_printer =
   let pr_alias_key key =
     try
       let prods = (KNmap.find key !prnotation_tab).pptac_prods in
-      let rec pr = function
+      let pr = function
       | TacTerm s -> primitive s
       | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
       in
@@ -314,7 +314,7 @@ type 'a extra_genarg_printer =
   | Extend.Uentry _ | Extend.Uentryl _ ->
     str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
 
-  let rec pr_targ prtac symb arg = match symb with
+  let pr_targ prtac symb arg = match symb with
   | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
     prtac (1, Any) arg
   | Extend.Uentryl (_, l) -> prtac (l, Any) arg
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index bcb28f77ce..a853576f25 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -136,7 +136,6 @@ let feedback_results results =
 let format_sec x = (Printf.sprintf "%.3fs" x)
 let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
 let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
-let padr n s = str s ++ ws (max 0 (n - utf8_length s))
 let padr_with c n s =
   let ulength = utf8_length s in
   str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 12a1566e20..5630a2d7b6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
 open Vars
 open Reduction
 open Tacticals.New
-open Tacmach
 open Tactics
 open Pretype_errors
 open Typeclasses
@@ -39,7 +38,7 @@ open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 
 (** Typeclass-based generalized rewriting. *)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 7a20838a27..6683d753bc 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -14,7 +14,6 @@ open Constrexpr
 open Tacexpr
 open Misctypes
 open Evd
-open Proof_type
 open Tacinterp
 
 (** TODO: document and clean me! *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 9c4ac52657..4a44f86d92 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open EConstr
 open Misctypes
 open Pattern
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cd8c9e471e..32750383b8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -15,7 +15,6 @@ open Genarg
 open Extend
 open Pcoq
 open Egramml
-open Egramcoq
 open Vernacexpr
 open Libnames
 open Nameops
@@ -88,9 +87,6 @@ let rec parse_user_entry s sep =
   else
     Uentry s
 
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
 let interp_entry_name interp symb =
   let rec eval = function
   | Ulist1 e -> Ulist1 (eval e)
@@ -320,7 +316,7 @@ let add_tactic_notation local n prods e =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local n prods false ids tac
+  add_glob_tactic_notation local ~level:n prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223aa..d1e2a7bbe6 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Genarg
 open Names
 open Tacexpr
 open Geninterp
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3f83f104e9..75227def0f 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,12 +118,6 @@ let intern_constr_reference strict ist = function
       GRef (loc,locate_global_with_alias lqid,None), 
 	if strict then None else Some (CRef (r,None))
 
-let intern_move_location ist = function
-  | MoveAfter id -> MoveAfter (intern_hyp ist id)
-  | MoveBefore id -> MoveBefore (intern_hyp ist id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 50f43931e9..b8c021f188 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -25,7 +25,6 @@ open Refiner
 open Tacmach.New
 open Tactic_debug
 open Constrexpr
-open Term
 open Termops
 open Tacexpr
 open Genarg
@@ -436,12 +435,6 @@ let interp_hyp_list_as_list ist env sigma (loc,id as x) =
 let interp_hyp_list ist env sigma l =
   List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l)
 
-let interp_move_location ist env sigma = function
-  | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id)
-  | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
   | ArgVar (loc, id) ->
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 1e5f6bd42b..494f36a95a 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Tactic_debug
-open Term
 open EConstr
 open Tacexpr
 open Genarg
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 7745d9b7b6..0b4d35a22a 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -10,7 +10,6 @@ open Environ
 open Pattern
 open Names
 open Tacexpr
-open Term
 open EConstr
 open Evd
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index dc7ee6a234..4de2081cf8 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -10,7 +10,6 @@ open Term
 open EConstr
 open Hipattern
 open Names
-open Pp
 open Geninterp
 open Misctypes
 open Tacexpr
@@ -242,7 +241,7 @@ let tauto_uniform_unit_flags = {
 }
 
 (* This is the compatibility mode (not used) *)
-let tauto_legacy_flags = {
+let _tauto_legacy_flags = {
   binary_mode = true;
   binary_mode_bugged_detection = true;
   strict_in_contravariant_hyp = true;
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index eb26c5431d..a36607ec38 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
 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index f4f9b3c2f1..3779944154 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 cc89e2b9d8..e1ceabe9e2 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 f54914f252..6b8b820ac6 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.               *)
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index b1ff59e780..a120d4efb2 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -153,7 +153,6 @@ module Make (P:Polynom.S) = struct
   type coef = P.t
   let coef0 = P.of_num (Num.Int 0)
   let coef1 = P.of_num (Num.Int 1)
-  let coefm1 = P.of_num (Num.Int (-1))
   let string_of_coef c = "["^(P.to_string c)^"]"
 
 (***********************************************************************
@@ -197,8 +196,6 @@ module Hashpol = Hashtbl.Make(
 
 (* A pretty printer for polynomials, with Maple-like syntax. *)
 
-open Format
-
 let getvar lv i =
   try (List.nth lv i)
   with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
@@ -252,59 +249,6 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
   in 
   (stringP p true)
 
-
-
-let print_pol zeroP hdP tlP coefterm monterm string_of_coef
-    dimmon string_of_exp lvar p =
-
-  let rec print_mon m coefone =
-    let s=ref [] in
-    for i=1 to (dimmon m) do
-      (match (string_of_exp m i) with
-        "0" -> ()
-      | "1" -> s:= (!s) @ [(getvar lvar (i-1))]
-      | e -> s:= (!s) @ [((getvar lvar (i-1)) ^ "^" ^ e)]);
-    done;
-    (match !s with
-      [] -> if coefone 
-      then print_string "1"
-      else ()
-    | l -> if coefone 
-    then print_string (String.concat "*" l)
-    else (print_string "*"; 
-          print_string (String.concat "*" l)))
-  and print_term t start = let a = coefterm t and m = monterm t in
-  match (string_of_coef a) with
-    "0" -> ()
-  | "1" ->(match start with
-      true -> print_mon m true
-    |false -> (print_string "+ ";
-               print_mon m true))
-  | "-1" ->(print_string "-";print_space();print_mon m true)
-  | c -> if (String.get c 0)='-'
-  then (print_string "- ";
-        print_string (String.sub c 1 
-                        ((String.length c)-1));
-        print_mon m false)
-  else (match start with
-    true -> (print_string c;print_mon m false)
-  |false -> (print_string "+ ";
-             print_string c;print_mon m false))
-  and printP p start = 
-    if (zeroP p)
-    then (if start 
-    then print_string("0")
-    else ())
-    else (print_term (hdP p) start;
-          if start then open_hovbox 0;
-          print_space();
-          print_cut();
-          printP (tlP p) false)
-  in open_hovbox 3;
-  printP p true;
-  print_flush()
-
-
 let stringP metadata (p : poly) =
   string_of_pol 
     (fun p -> match p with [] -> true | _ -> false)
@@ -595,9 +539,6 @@ let addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat decon
  critical pairs/s-polynomials
  *)
 
-let ordcpair ((i1,j1),m1) ((i2,j2),m2) =
-  compare_mon m1 m2 
-
 module CPair =
 struct
 type t = (int * int) * Monomial.t
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index db8f3e4b21..632b9dac14 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -22,7 +22,6 @@ open Utile
 let num_0 = Int 0
 and num_1 = Int 1
 and num_2 = Int 2
-and num_10 = Int 10
 
 let numdom r =
   let r' = Ratio.normalize_ratio (ratio_of_num r) in
@@ -35,7 +34,6 @@ module BigInt = struct
   type t = big_int
   let of_int = big_int_of_int
   let coef0 = of_int 0
-  let coef1 = of_int 1
   let of_num = Num.big_int_of_num
   let to_num = Num.num_of_big_int
   let equal = eq_big_int
@@ -49,7 +47,6 @@ module BigInt = struct
   let div = div_big_int
   let modulo = mod_big_int
   let to_string = string_of_big_int
-  let to_int x = int_of_big_int x
   let hash x =
     try (int_of_big_int x)
     with Failure _ -> 1
@@ -61,15 +58,6 @@ module BigInt = struct
     then a
     else if lt a b then pgcd b a else pgcd b (modulo a b)
 
-
-  (* signe du pgcd = signe(a)*signe(b) si non nuls. *)
-  let pgcd2 a b =
-    if equal a coef0 then b
-    else if equal b coef0 then a
-    else let c = pgcd (abs a) (abs b) in
-    if ((lt coef0 a)&&(lt b coef0))
-      ||((lt coef0 b)&&(lt a coef0))
-    then opp c else c
 end
 
 (*
@@ -146,8 +134,6 @@ let mul = function
   | (Const n,q) when eq_num n num_1 -> q
   | (p,q) -> Mul(p,q)
 
-let unconstr = mkRel 1
-
 let tpexpr =
   lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
 let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc")
@@ -271,20 +257,6 @@ let set_nvars_term nvars t =
     | Pow (t1,n) ->  aux t1 nvars
   in aux t nvars
 
-let string_of_term p =
-  let rec aux p =
-    match p with
-    | Zero -> "0"
-    | Const r -> string_of_num r
-    | Var v -> "x"^v
-    | Opp t1 -> "(-"^(aux t1)^")"
-    | Add (t1,t2) -> "("^(aux t1)^"+"^(aux t2)^")"
-    | Sub (t1,t2) ->  "("^(aux t1)^"-"^(aux t2)^")"
-    | Mul (t1,t2) ->  "("^(aux t1)^"*"^(aux t2)^")"
-    | Pow (t1,n) ->  (aux t1)^"^"^(string_of_int n)
-  in aux p
-
-
 (***********************************************************************
    Coefficients: recursive polynomials
  *)
@@ -437,7 +409,7 @@ open Ideal
    that has the same size than lp and where true indicates an
    element that has been removed
  *)
-let rec clean_pol lp =
+let clean_pol lp =
   let t = Hashpol.create 12 in
   let find p = try Hashpol.find t p 
                with 
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index bd991a955c..334b03de1d 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -330,11 +330,13 @@ let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
 let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
   let e = original.body in
   let sigma = new_var_id () in
+  if e == [] then begin
+    display_system print_var [original] ; failwith "TL"
+    end;
   let smallest,var =
-    try
-      List.fold_left (fun (v,p) c ->  if v >? (abs c.c) then abs c.c,c.v else (v,p))
-              (abs (List.hd e).c, (List.hd e).v) (List.tl e)
-    with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+    List.fold_left (fun (v,p) c ->  if v >? (abs c.c) then abs c.c,c.v else (v,p))
+      (abs (List.hd e).c, (List.hd e).v) (List.tl e)
+  in
   let m = smallest + one in
   let new_eq =
     { constant = omega_mod original.constant m;
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index dd68eac24c..d59ffee546 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -19,7 +19,6 @@ open Environ
 open Libnames
 open Globnames
 open Glob_term
-open Tacticals
 open Tacexpr
 open Coqlib
 open Mod_subst
@@ -279,8 +278,6 @@ let my_constant c =
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
-let new_ring_path =
-  DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 4367d021c0..d9d32c681d 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -7,13 +7,10 @@
 (************************************************************************)
 
 open Names
-open Constr
 open EConstr
 open Libnames
 open Globnames
 open Constrexpr
-open Tacexpr
-open Proof_type
 open Newring_ast
 
 val protect_tac_in : string -> Id.t -> unit Proofview.tactic
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f3555ebc4c..72c70750c9 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -21,30 +21,21 @@ open Pp
 open Pcoq
 open Genarg
 open Stdarg
-open Tacarg
 open Term
 open Vars
-open Topconstr
 open Libnames
 open Tactics
 open Tacticals
 open Termops
-open Namegen
 open Recordops
 open Tacmach
-open Coqlib
 open Glob_term
 open Util
 open Evd
-open Extend
-open Goptions
 open Tacexpr
-open Proofview.Notations
 open Tacinterp
 open Pretyping
 open Constr
-open Pltac
-open Extraargs
 open Ppconstr
 open Printer
 
@@ -54,14 +45,9 @@ open Decl_kinds
 open Evar_kinds
 open Constrexpr
 open Constrexpr_ops
-open Notation_term
-open Notation_ops
-open Locus
-open Locusops
 
 DECLARE PLUGIN "ssrmatching_plugin"
 
-type loc = Loc.t
 let dummy_loc = Loc.ghost
 let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
 let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
@@ -90,8 +76,6 @@ let pp s = !pp_ref s
 let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
   match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |]
-let get_index = function ArgArg i -> i | _ ->
-  CErrors.anomaly (str"Uninterpreted index")
 (* Toplevel constr must be globalized twice ! *)
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -304,8 +288,6 @@ let unif_EQ_args env sigma pa a =
 
 let unif_HO env ise p c = Evarconv.the_conv_x env p c ise
 
-let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise
-
 let unif_HO_args env ise0 pa i ca =
   let n = Array.length pa in
   let rec loop ise j =
@@ -371,11 +353,6 @@ let unif_end env sigma0 ise0 pt ok =
     let s, uc', t = nf_open_term sigma0 ise2 t in
     s, Evd.union_evar_universe_context uc uc', t
 
-let pf_unif_HO gl sigma pt p c =
-  let env = pf_env gl in
-  let ise = unif_HO env (create_evar_defs sigma) p c in
-  unif_end env (project gl) ise pt (fun _ -> true)
-
 let unify_HO env sigma0 t1 t2 =
   let sigma = unif_HO env sigma0 t1 t2 in
   let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in
@@ -440,16 +417,10 @@ let all_ok _ _ = true
 let proj_nparams c =
   try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
 
-let isFixed c = match kind_of_term c with
-  | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
-  | _ -> false
-
 let isRigid c = match kind_of_term c with
   | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
   | _ -> false
 
-exception UndefPat
-
 let hole_var = mkVar (id_of_string "_")
 let pr_constr_pat c0 =
   let rec wipe_evar c =
@@ -917,13 +888,6 @@ let pp_pattern (sigma, p) =
 let pr_cpattern = pr_term
 let pr_rpattern _ _ _ = pr_pattern
 
-let pr_option f = function None -> mt() | Some x -> f x
-let pr_ssrpattern _ _ _ = pr_option pr_pattern
-let pr_pattern_squarep = pr_option (fun r -> str "[" ++ pr_pattern r ++ str "]")
-let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep
-let pr_pattern_roundp = pr_option (fun r -> str "(" ++ pr_pattern r ++ str ")")
-let pr_ssrpattern_roundp  _ _ _ = pr_pattern_roundp
-
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
 let glob_ssrterm gs = function
@@ -1045,7 +1009,6 @@ let interp_wit wit ist gl x =
   let arg = interp_genarg ist globarg in
   let (sigma, arg) = of_ftactic arg gl in
   sigma, Value.cast (topwit wit) arg
-let interp_constr = interp_wit wit_constr
 let interp_open_constr ist gl gc =
   interp_wit wit_open_constr ist gl gc
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
@@ -1261,7 +1224,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in
     let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in
     let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in
-    let concl = find_T env0 concl0 1 do_subst in
+    let concl = find_T env0 concl0 1 ~k:do_subst in
     let _ = end_T () in
     concl
   | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) ->
@@ -1273,11 +1236,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     (* we start from sigma, so hole is considered a rigid head *)
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in
-    let concl = find_T env0 concl0 1 (fun env c _ h ->
+    let concl = find_T env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
       fs p_sigma (find_X env (fs sigma p) h 
-        (fun env _ -> do_subst env e_body))) in
+        ~k:(fun env _ -> do_subst env e_body))) in
     let _ = end_X () in let _ = end_T () in 
     concl
   | Some (sigma, E_In_X_In_T (e, hole, p)) ->
@@ -1289,11 +1252,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_X, end_X = mk_tpattern_matcher sigma noindex holep in
     let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in
     let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in
-    let concl = find_T env0 concl0 1 (fun env c _ h ->
+    let concl = find_T env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
-        find_E env e_body h do_subst))) in
+      fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h ->
+        find_E env e_body h ~k:do_subst))) in
     let _ = end_E () in let _ = end_X () in let _ = end_T () in
     concl
   | Some (sigma, E_As_X_In_T (e, hole, p)) ->
@@ -1306,10 +1269,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher sigma occ holep in
-    let concl = find_TE env0 concl0 1 (fun env c _ h ->
+    let concl = find_TE env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
+      fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h ->
         let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in
         let e_body = fs e_sigma e in
         do_subst env e_body e_body h))) in
@@ -1352,7 +1315,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let ise, u = mk_tpattern env sigma0 (ise,EConstr.Unsafe.to_constr t) ok L2R p in
  let find_U, end_U =
    mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
- let concl = find_U env concl h (fun _ _ _ -> mkRel) in
+ let concl = find_U env concl h ~k:(fun _ _ _ -> mkRel) in
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx
 
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 894cdb9438..638b4e254e 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -4,7 +4,6 @@
 open Genarg
 open Tacexpr
 open Environ
-open Tacmach
 open Evd
 open Proof_type
 open Term
@@ -226,7 +225,6 @@ val loc_of_cpattern : cpattern -> Loc.t
 val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern
-val cpattern_of_id : Names.variable -> cpattern
 val pr_constr_pat : constr -> Pp.std_ppcmds
 val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma
 val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma