From 18ebb3f525a965358d96eab7df493450009517b5 Mon Sep 17 00:00:00 2001
From: regisgia
Date: Fri, 14 Sep 2012 09:52:38 +0000
Subject: The new ocaml compiler (4.00) has a lot of very cool warnings,
 especially about unused definitions, unused opens and unused rec flags.

The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.

(a) "unused rec flags". They cannot change the semantics of the program
    but only allow the inliner to do a better job.

(b) "unused type definitions". I only removed type definitions that were
    given to functors that do not require them. Some type definitions were
    used as documentation to obtain better error messages, but were not
    ascribed to any definition. I superficially mentioned them in one
    arbitrary chosen definition to remove the warning. This is unaesthetic
    but I did not find a better way.

(c) "unused for loop index". The following idiom of imperative
    programming is used at several places: "for i = 1 to n do
    that_side_effect () done".  I replaced "i" with "_i" to remove the
    warning... but, there is a combinator named "Util.repeat" that
    would only cost us a function call while improving readibility.
    Should'nt we use it?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation_ops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ad1bd11381..ae851d8ba3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -110,7 +110,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
   | NPatVar n -> GPatVar (loc,(false,n))
   | NRef x -> GRef (loc,x)
 
-let rec glob_constr_of_notation_constr loc x =
+let glob_constr_of_notation_constr loc x =
   let rec aux () x =
     glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x
   in aux () x
@@ -544,7 +544,7 @@ let rec match_iterated_binders islambda decls = function
 let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
   (List.remove_assoc x sigmavar,sigmalist,sigmabinders)
 
-let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin =
+let match_abinderlist_with_app match_fun metas sigma rest x iter termin =
   let rec aux sigma acc rest =
     try
       let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
-- 
cgit v1.2.3