Merge PR#582: Fix warnings

24 files changed, 15 insertions, 30 deletions

diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index b014af2c7f..eb25994bef 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open CClosure
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index e9b3d197bc..32da81f96c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,6 @@ open Nametab
 open Environ
 open Libobject
 open Term
-open Termops
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 0d741a5a5d..c4238e8b0d 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open EConstr
 open Evd
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 542db7fdfa..c26e7458e6 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -22,7 +22,6 @@ open Environ
 open EConstr
 open Vars
 open Reductionops
-open Typeops
 open Pretype_errors
 open Classops
 open Evarutil
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index bc63d092d9..ea3d3f0fa1 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -8,7 +8,6 @@
 
 open Evd
 open Names
-open Term
 open Environ
 open EConstr
 open Glob_term
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d553506228..2334be9664 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -87,7 +87,6 @@ let rec build_lambda sigma vars ctx m = match vars with
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
-  let len = List.length ctx in
   let pre, suf = List.chop (pred n) ctx in
   let (na, t, suf) = match suf with
   | [] -> assert false
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8ba4086795..483e2b4320 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -13,7 +13,6 @@ open CErrors
 open Util
 open Names
 open Term
-open Environ
 open EConstr
 open Vars
 open Inductiveops
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4bb66b8e91..305eae15a3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -21,7 +21,6 @@ open Recordops
 open Evarutil
 open Evardefine
 open Evarsolve
-open Globnames
 open Evd
 open Pretype_errors
 open Sigma.Notations
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index fc07f0fbea..7cee1e8a7e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open Reductionops
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index c5ae684e3b..5fd104c781 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 77086d046c..f0d0114775 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
 open Util
 open CErrors
 open Names
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index e3d3b74f10..d22f94e4e5 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Locus
-open Term
 open Evd
 open Pretype_errors
 open Environ
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5b42add285..429e5005ec 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -459,7 +459,6 @@ let extract_mrectype sigma t =
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let open EConstr in
   let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b16d044956..33a68589c1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -20,7 +20,6 @@ open Mod_subst
 open Misctypes
 open Decl_kinds
 open Pattern
-open Evd
 open Environ
 
 let case_info_pattern_eq i1 i2 =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 5694d345c1..791fd74ed3 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Globnames
 open Glob_term
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 24f6d16899..f9cf6b83bc 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ae87cd8c02..68ef976592 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -33,7 +33,6 @@ open EConstr
 open Vars
 open Reductionops
 open Type_errors
-open Typeops
 open Typing
 open Globnames
 open Nameops
@@ -195,7 +194,7 @@ let _ =
 (** Miscellaneous interpretation functions *)
 let interp_universe_level_name evd (loc,s) =
   let names, _ = Global.global_universe_names () in
-    if CString.string_contains s "." then
+    if CString.string_contains ~where:s ~what:"." then
       match List.rev (CString.split '.' s) with
       | [] -> anomaly (str"Invalid universe name " ++ str s)
       | n :: dp -> 
diff --git a/pretyping/program.ml b/pretyping/program.ml
index caa5a5c8a6..42acc5705b 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2703205386..52f424f751 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -239,6 +239,9 @@ sig
   | Shift of int
   | Update of 'a
   and 'a t = 'a member list
+
+  exception IncompatibleFold2
+
   val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
   val empty : 'a t
   val is_empty : 'a t -> bool
@@ -413,6 +416,7 @@ struct
       | (_,_) -> false in
     compare_rec 0 stk1 stk2
 
+  exception IncompatibleFold2
   let fold2 f o sk1 sk2 =
     let rec aux o lft1 sk1 lft2 sk2 =
       let fold_array =
@@ -442,7 +446,7 @@ struct
 	  aux o lft1 (List.rev params1) lft2 (List.rev params2)
 	in aux o' lft1' q1 lft2' q2
       | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
-	raise (Invalid_argument "Reductionops.Stack.fold2")
+	raise IncompatibleFold2
     in aux o 0 (List.rev sk1) 0 (List.rev sk2)
 
   let rec map f x = List.map (function
@@ -1117,7 +1121,9 @@ let local_whd_state_gen flags sigma =
   whrec
 
 let raw_whd_state_gen flags env =
-  let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in
+  let f sigma s = fst (whd_state_gen ~refold:(get_refolding_in_reduction ())
+                         ~tactic_mode:false
+                         flags env sigma s) in
   f
 
 let stack_red_of_state_red f =
@@ -1127,7 +1133,7 @@ let stack_red_of_state_red f =
 (* Drops the Cst_stack *)
 let iterate_whd_gen refold flags env sigma s =
   let rec aux t =
-  let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
+  let (hd,sk),_ = whd_state_gen ~refold ~tactic_mode:false flags env sigma (t,Stack.empty) in
   let whd_sk = Stack.map aux sk in
   Stack.zip sigma ~refold (hd,whd_sk)
   in aux s
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 752c30a8ac..af80481569 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -81,8 +81,11 @@ module Stack : sig
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
 
   val compare_shape : 'a t -> 'a t -> bool
+
+  exception IncompatibleFold2
   (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
-      @return the result and the lifts to apply on the terms *)
+      @return the result and the lifts to apply on the terms
+      @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *)
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
     constr t -> constr t -> 'a * int * int
   val map : ('a -> 'a) -> 'a t -> 'a t
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 76d0bc241f..c31212e26a 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open Evd
 open EConstr
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 2db0e9e881..754dacd193 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 9bd430e4d6..558575ccce 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,7 +8,6 @@
 
 open Loc
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 532cc8baa5..661c1d8657 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1095,7 +1095,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       let app = mkApp (c, Array.rev_of_list ks) in
       (* let substn = unirec_rec curenvnb pb b false substn t cN in *)
 	unirec_rec curenvnb pb opt' substn c1 app
-      with Invalid_argument "Reductionops.Stack.fold2" ->
+      with Reductionops.Stack.IncompatibleFold2 ->
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
   in
@@ -1535,9 +1535,6 @@ let indirectly_dependent sigma c d decls =
        way to see that the second hypothesis depends indirectly over 2 *)
     List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
 
-let indirect_dependency sigma d decls =
-  decls  |>  List.filter (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d)  |>  List.hd  |>  NamedDecl.get_id
-
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let current_sigma = Sigma.to_evar_map current_sigma in
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in