From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 25 Apr 2017 14:31:15 +0200 Subject: Fix 4.04 warnings --- engine/evd.ml | 2 +- interp/notation.ml | 1 - kernel/constr.ml | 22 ---------------------- lib/cErrors.ml | 2 ++ parsing/pcoq.ml | 1 - plugins/firstorder/g_ground.ml4 | 1 - plugins/funind/functional_principles_proofs.ml | 5 +++-- plugins/funind/indfun_common.ml | 9 +++------ plugins/funind/invfun.ml | 10 +++++----- plugins/funind/recdef.ml | 5 +++-- plugins/ltac/rewrite.ml | 2 +- plugins/ltac/tauto.ml | 1 - plugins/omega/omega.ml | 10 ++++++---- pretyping/evarsolve.ml | 1 - pretyping/reductionops.ml | 6 +++++- pretyping/reductionops.mli | 5 ++++- pretyping/unification.ml | 2 +- printing/prettyp.ml | 2 +- stm/stm.ml | 3 +++ stm/vcs.ml | 2 -- tools/coqwc.mll | 2 ++ 21 files changed, 40 insertions(+), 54 deletions(-) diff --git a/engine/evd.ml b/engine/evd.ml index 6b1e1a855..db048bbd6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -15,7 +15,7 @@ open Term open Vars open Environ -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) module NamedDecl = Context.Named.Declaration (** Generic filters *) diff --git a/interp/notation.ml b/interp/notation.ml index 90ac7f729..6aa6f54c0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -22,7 +22,6 @@ open Glob_ops open Ppextend open Context.Named.Declaration -module NamedDecl = Context.Named.Declaration (*i*) (*s A scope is a set of notations; it includes diff --git a/kernel/constr.ml b/kernel/constr.ml index 5a7561bf5..71efe9032 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -978,28 +978,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash) let case_info_hash = CaseinfoHash.hash -module Hsorts = - Hashcons.Make( - struct - open Sorts - - type t = Sorts.t - type u = universe -> universe - let hashcons huniv = function - Prop c -> Prop c - | Type u -> Type (huniv u) - let eq s1 s2 = - s1 == s2 || - match (s1,s2) with - (Prop c1, Prop c2) -> c1 == c2 - | (Type u1, Type u2) -> u1 == u2 - |_ -> false - let hash = function - | Prop Null -> 0 | Prop Pos -> 1 - | Type u -> 2 + Universe.hash u - end) - -(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *) let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind let hcons = diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1c1ff7e2f..b55fd80c6 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -121,12 +121,14 @@ end by inner functions during a [vernacinterp]. They should be handled only at the very end of interp, to be displayed to the user. *) +[@@@ocaml.warning "-52"] let noncritical = function | Sys.Break | Out_of_memory | Stack_overflow | Assert_failure _ | Match_failure _ | Anomaly _ | Timeout | Drop | Quit -> false | Invalid_argument "equal: functional value" -> false | _ -> true +[@@@ocaml.warning "+52"] (** Check whether an exception is handled *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 3f014c4c8..9a4766c0b 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open CErrors open Util open Extend diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 8ef6a09d0..b25017535 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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index df81bc78c..55d361e3d 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -229,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 @@ -536,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/indfun_common.ml b/plugins/funind/indfun_common.ml index c6f5c2745..848b44a60 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 diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 29472cdef..6c0c28905 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1025,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 @@ -1040,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/recdef.ml b/plugins/funind/recdef.ml index 1e405d2c9..bd30f1159 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/rewrite.ml b/plugins/ltac/rewrite.ml index 12a1566e2..9a1615d3f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -39,7 +39,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/tauto.ml b/plugins/ltac/tauto.ml index e86d1c728..4de2081cf 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 diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index bd991a955..334b03de1 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/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 77086d046..f0d011477 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/reductionops.ml b/pretyping/reductionops.ml index da3add2e5..52f424f75 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 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 752c30a8a..af8048156 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/unification.ml b/pretyping/unification.ml index 4a3836d86..661c1d865 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 diff --git a/printing/prettyp.ml b/printing/prettyp.ml index aa422e36a..381af83c7 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -29,7 +29,7 @@ open Printer open Printmod open Context.Rel.Declaration -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) module NamedDecl = Context.Named.Declaration type object_pr = { diff --git a/stm/stm.ml b/stm/stm.ml index 8c1185b6d..84c8aa9a9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1205,6 +1205,8 @@ let detect_proof_block id name = (****************************** THE SCHEDULER *********************************) (******************************************************************************) +(* Unused module warning doesn't understand [module rec] *) +[@@@ocaml.warning "-60"] module rec ProofTask : sig type competence = Stateid.t list @@ -2318,6 +2320,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach ~redefine_qed id end (* }}} *) +[@@@ocaml.warning "+60"] (********************************* STM API ************************************) (******************************************************************************) diff --git a/stm/vcs.ml b/stm/vcs.ml index d3886464d..88f860eb6 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -74,8 +74,6 @@ module Dag = Dag.Make(OT) type id = OT.t -module NodeSet = Dag.NodeSet - module Branch = struct type t = string diff --git a/tools/coqwc.mll b/tools/coqwc.mll index b4fc738d0..cd07d4216 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -239,6 +239,7 @@ let process_channel ch = if !skip_header then read_header lb; spec lb +[@@@ocaml.warning "-52"] let process_file f = try let ch = open_in f in @@ -251,6 +252,7 @@ let process_file f = flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr | Sys_error s -> flush stdout; eprintf "coqwc: %s\n" s; flush stderr +[@@@ocaml.warning "+52"] (*s Parsing of the command line. *) -- cgit v1.2.3