Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 7 insertions, 21 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 88983637a..eb767694b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -268,8 +268,6 @@ lorque source est None alors target est None aussi.
 
 let add_new_coercion_core coef stre source target isid =
   check_source source;
-  let env = Global.env () in
-  let v = constr_of_global coef in
   let t = Global.type_of_global coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let tg,lp = prods_of t in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2da3e2cf5..0a97baf8b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -171,7 +171,7 @@ let assumption_message id =
 let declare_one_assumption is_coe (local,kind) c (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
-        let r = 
+        let _ = 
           declare_variable ident 
             (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in
         assumption_message ident;
@@ -279,8 +279,7 @@ let interp_mutual lparams lnamearconstrs finite =
       [] lnamearconstrs in
   if not (list_distinct allnames) then
     error "Two inductive objects have the same name";
-  let nparams = local_binders_length lparams
-  and sigma = Evd.empty 
+  let sigma = Evd.empty 
   and env0 = Global.env() in
   let env_params, params =
     List.fold_left
@@ -313,8 +312,6 @@ let interp_mutual lparams lnamearconstrs finite =
   let paramassums = 
     List.fold_right (fun d l -> match d with
 	(id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in
-  let indnames =
-    List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
   let nparamassums = List.length paramassums in
   let (ind_env,ind_impls,arityl) =
     List.fold_left
@@ -432,7 +429,7 @@ let extract_coe_la_lc = function
 let build_mutual lind finite =
   let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in
   let notations,mie = interp_mutual lparams lnamearconstructs finite in
-  let kn = declare_mutual_with_eliminations false mie in
+  let _ = declare_mutual_with_eliminations false mie in
   (* Declare the notations now bound to the inductive types *)
   List.iter (fun (df,c,scope) ->
     Metasyntax.add_notation_interpretation df [] c scope) notations;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cc3740501..56f6b111e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -129,7 +129,6 @@ let re_exec is_ide =
   let s = !re_exec_version in
   let is_native = (Mltop.get()) = Mltop.Native in
   let prog = Sys.argv.(0) in
-  let coq = Filename.basename prog in
   if (is_native && s = "byte") || ((not is_native) && s = "opt")
   then begin
     let s = if s = "" then if is_native then "opt" else "byte" else s in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8b72d5b01..55201ea43 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -84,7 +84,6 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
   let ctx = make_all_name_different ctx in
   let pi = pr_inductive ctx ind in
   let pc = prterm_env ctx c in
-  let ppt = prterm_env ctx pj.uj_type in
   let msg = match okinds with
   | Some(kp,ki,explanation) ->
       let pki = prterm_env ctx ki in
@@ -380,7 +379,6 @@ let explain_var_not_found ctx id =
   spc ()  ++ str "in the current" ++ spc ()  ++ str "environment"
 
 let explain_wrong_case_info ctx ind ci =
-  let ctx = make_all_name_different ctx in
   let pi = prterm (mkInd ind) in
   if ci.ci_ind = ind then
     str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++
@@ -646,8 +644,8 @@ let explain_needs_inversion ctx x t =
   px  ++ str " of type: " ++ pt
 
 let explain_unused_clause env pats =
-  let s = if List.length pats > 1 then "s" else "" in
 (* Without localisation
+  let s = if List.length pats > 1 then "s" else "" in
   (str ("Unused clause with pattern"^s) ++ spc () ++
     hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
 *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a99a15b35..498b21f7f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -201,7 +201,6 @@ let check_entry_type (u,n) =
     | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
 
 let add_grammar_obj univ entryl =
-  let u = create_univ_if_new univ in
   let g = interp_grammar_command univ check_entry_type entryl in
   Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g))
 
@@ -662,12 +661,12 @@ let read_recursive_format sl fmt =
   let slfmt, fmt = get_head fmt in
   slfmt, get_tail (slfmt, fmt)
 
-let hunks_of_format (from,(vars,typs) as vt) symfmt = 
+let hunks_of_format (from,(vars,typs)) symfmt = 
   let rec aux = function
   | symbs, (UnpTerminal s' as u) :: fmt
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
-  | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt
+  | Terminal s :: symbs, (UnpTerminal s') :: fmt
       when s = unquote_notation_token s' ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
@@ -811,7 +810,6 @@ let pr_arg_level from = function
   | (n,_) -> str "Unknown level"
 
 let pr_level ntn (from,args) =
-  let lopen = ntn.[0] = '_' and ropen = ntn.[String.length ntn - 1] = '_' in
 (*
   let ppassoc, args = match args with
     | [] -> mt (), []
@@ -1350,7 +1348,6 @@ let add_notation local c dfmod mv8 sc =
                   add_notation_in_scope local df c modifiers mv8 sc toks
 	  | Some n ->
 	    (* Declare both syntax and interpretation *)
-	    let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
             add_notation_in_scope local df c modifiers mv8 sc toks
 
 (* TODO add boxes information in the expression *)
@@ -1410,7 +1407,6 @@ let add_infix local (inf,modl) pr mv8 sc =
       let (recs,vars,symbs) = analyse_notation_tokens toks in
       let (acvars,ac) = interp_aconstr [] vars a in
       let a' = (remove_vars recs acvars,ac) in
-      let a_for_old = interp_global_rawconstr_with_vars vars a in
       add_notation_interpretation_core local symbs None df a' sc 
 	onlyparse true None
     else
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 926d3e73b..124ad03c6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -64,7 +64,6 @@ let cl_of_qualid = function
 
 let show_proof () =
   let pts = get_pftreestate () in
-  let pf = proof_of_pftreestate pts in
   let cursor = cursor_of_pftreestate pts in
   let evc = evc_of_pftreestate pts in
   let (pfterm,meta_types) = extract_open_pftreestate pts in
@@ -1096,8 +1095,7 @@ let vernac_show = function
 
 let vernac_check_guard () =
   let pts = get_pftreestate () in
-  let pf = proof_of_pftreestate pts 
-  and cursor = cursor_of_pftreestate pts in
+  let pf = proof_of_pftreestate pts in
   let (pfterm,_) = extract_open_pftreestate pts in
   let message = 
     try