From 4abb41d008fc754f21916dcac9cce49f2d04dd6d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 24 Apr 2017 19:25:48 +0200 Subject: [toplevel] Use exception information for error printing. This is a partial backtrack on 63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we disregarded exception and tried to print error messages just by listening to feedback. However, feedback error messages are not always emitted due to https://coq.inria.fr/bugs/show_bug.cgi?id=5479 Thus meanwhile it is safer to go back to printing the information present in exceptions until we tweak the STM. This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many other glitches not reported, such errors in nested proofs. --- vernac/topfmt.ml | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'vernac/topfmt.ml') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index c25dd55fb..a1835959c 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -260,6 +260,29 @@ let init_color_output () = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning + +(* This is specific to the toplevel *) +let pr_loc loc = + if Loc.is_ghost loc then str"" + else + let fname = loc.Loc.fname in + if CString.equal fname "" then + Loc.(str"Toplevel input, characters " ++ int loc.bp ++ + str"-" ++ int loc.ep ++ str":") + else + Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ + str", line " ++ int loc.line_nb ++ str", characters " ++ + int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ + str":") + +let print_err_exn ?extra any = + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg_loc = pr_loc (Option.default Loc.ghost loc) in + let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in + let msg = CErrors.iprint (e, info) ++ fnl () in + std_logger ~pre_hdr Feedback.Error msg + (* Output to file, used only in extraction so a candidate for removal *) let ft_logger old_logger ft ?loc level mesg = let id x = x in -- cgit v1.2.3 From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- checker/closure.ml | 16 -------- checker/declarations.ml | 11 ----- checker/inductive.ml | 7 ---- checker/typeops.ml | 3 -- checker/univ.ml | 7 ---- engine/termops.ml | 24 ----------- ide/coqOps.ml | 3 -- ide/ideutils.ml | 11 ----- interp/notation_ops.ml | 4 -- kernel/names.ml | 2 - kernel/uGraph.mli | 3 ++ kernel/univ.ml | 4 -- lib/feedback.ml | 2 - lib/stateid.ml | 1 - parsing/cLexer.ml4 | 8 ---- parsing/egramcoq.ml | 4 -- parsing/g_vernac.ml4 | 5 --- parsing/pcoq.ml | 7 ---- plugins/funind/functional_principles_proofs.ml | 6 --- plugins/ltac/extratactics.ml4 | 2 - plugins/ltac/profile_ltac.ml | 1 - plugins/ltac/tacentries.ml | 3 -- plugins/ltac/tacintern.ml | 6 --- plugins/ltac/tacinterp.ml | 6 --- plugins/nsatz/ideal.ml | 57 -------------------------- plugins/nsatz/nsatz.ml | 28 ------------- plugins/setoid_ring/newring.ml | 2 - plugins/ssrmatching/ssrmatching.ml4 | 21 ---------- plugins/ssrmatching/ssrmatching.mli | 1 - pretyping/unification.ml | 3 -- printing/ppconstr.ml | 4 -- printing/ppvernac.ml | 4 -- printing/printer.ml | 5 --- proofs/clenv.ml | 5 --- proofs/logic.ml | 5 --- proofs/tacmach.ml | 3 -- stm/stm.ml | 7 ---- tactics/hipattern.ml | 1 - tactics/tactics.ml | 2 - tools/coqdoc/output.mli | 1 - toplevel/vernac.ml | 1 - vernac/auto_ind_decl.ml | 2 - vernac/metasyntax.ml | 2 +- vernac/record.ml | 2 +- vernac/topfmt.ml | 12 ------ 45 files changed, 5 insertions(+), 309 deletions(-) (limited to 'vernac/topfmt.ml') diff --git a/checker/closure.ml b/checker/closure.ml index cef1d31a6..b8294e795 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -651,22 +651,6 @@ let drop_parameters depth n argstk = (** Projections and eta expansion *) -let rec get_parameters depth n argstk = - match argstk with - Zapp args::s -> - let q = Array.length args in - if n > q then Array.append args (get_parameters depth (n-q) s) - else if Int.equal n q then [||] - else Array.sub args 0 n - | Zshift(k)::s -> - get_parameters (depth-k) n s - | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - if Int.equal n 0 then [||] - else raise Not_found (* Trying to eta-expand a partial application..., should do - eta expansion first? *) - | _ -> assert false - (* strip_update_shift_app only produces Zapp and Zshift items *) - let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.mind_record with diff --git a/checker/declarations.ml b/checker/declarations.ml index 56d437c16..ad93146d5 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -463,13 +463,6 @@ let is_opaque cb = match cb.const_body with let opaque_univ_context cb = force_lazy_constr_univs cb.const_body -let subst_rel_declaration sub (id,copt,t as x) = - let copt' = Option.smartmap (subst_mps sub) copt in - let t' = subst_mps sub t in - if copt == copt' && t == t' then x else (id,copt',t') - -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) - let subst_recarg sub r = match r with | Norec -> r | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in @@ -517,10 +510,6 @@ let subst_decl_arity f g sub ar = if x' == x then ar else TemplateArity x' -let map_decl_arity f g = function - | RegularArity a -> RegularArity (f a) - | TemplateArity a -> TemplateArity (g a) - let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) diff --git a/checker/inductive.ml b/checker/inductive.ml index ae2f7de8a..8f23a38af 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -436,13 +436,6 @@ let eq_recarg r1 r2 = match r1, r2 with let eq_wf_paths = Rtree.equal eq_recarg -let pp_recarg = function - | Norec -> Pp.str "Norec" - | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) - | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) - -let pp_wf_paths = Rtree.pp_tree pp_recarg - let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 diff --git a/checker/typeops.ml b/checker/typeops.ml index 173e19ce1..02d801741 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -85,9 +85,6 @@ let type_of_constant_knowing_parameters env cst paramtyps = let type_of_constant_type env t = type_of_constant_type_knowing_parameters env t [||] -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = let _cb = try lookup_constant kn env diff --git a/checker/univ.ml b/checker/univ.ml index 668f3a058..fb1a0faa7 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -87,7 +87,6 @@ module HList = struct val exists : (elt -> bool) -> t -> bool val for_all : (elt -> bool) -> t -> bool val for_all2 : (elt -> elt -> bool) -> t -> t -> bool - val remove : elt -> t -> t val to_list : t -> elt list end @@ -128,12 +127,6 @@ module HList = struct | Nil -> [] | Cons (x, _, l) -> x :: to_list l - let rec remove x = function - | Nil -> nil - | Cons (y, _, l) -> - if H.eq x y then l - else cons y (remove x l) - end end diff --git a/engine/termops.ml b/engine/termops.ml index 64f4c6dc5..29dcddbb0 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -612,30 +612,6 @@ let adjust_app_array_size f1 l1 f2 l2 = let extras,restl1 = Array.chop (len1-len2) l1 in (mkApp (f1,extras), restl1, f2, l2) -(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate - subterms of [c]; it carries an extra data [l] (typically a name - list) which is processed by [g na] (which typically cons [na] to - [l]) at each binder traversal (with name [na]); it is not recursive - and the order with which subterms are processed is not specified *) - -let map_constr_with_named_binders g f l c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (c,k,t) -> mkCast (f l c, k, f l t) - | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c) - | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) - | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) - | App (c,al) -> mkApp (f l c, Array.map (f l) al) - | Proj (p,c) -> mkProj (p, f l c) - | Evar (e,al) -> mkEvar (e, Array.map (f l) al) - | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl) - | Fix (ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - | CoFix(ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 259557f40..b180aa556 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -128,9 +128,6 @@ end = struct end open SentenceId -let log_pp msg : unit task = - Coq.lift (fun () -> Minilib.log_pp msg) - let log msg : unit task = Coq.lift (fun () -> Minilib.log msg) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d7d38a5ec..a08ab07b5 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -35,17 +35,6 @@ let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) -let xml_to_string xml = - let open Xml_datatype in - let buf = Buffer.create 1024 in - let rec iter = function - | PCData s -> Buffer.add_string buf s - | Element (_, _, children) -> - List.iter iter children - in - let () = iter xml in - Buffer.contents buf - let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that it has to reimplement its own helper function. Unluckily, it relies on diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 8b4fadb5a..d08fb107b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1141,10 +1141,6 @@ let term_of_binder = function | Name id -> GVar (Loc.ghost,id) | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) -type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.binding_kind * - glob_constr option * glob_constr - let match_notation_constr u c (metas,pat) = let terms,binders,termlists,binderlists = match_ false u ([],[]) metas ([],[],[],[]) c pat in diff --git a/kernel/names.ml b/kernel/names.ml index 5c10badbe..811b4a62a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -542,7 +542,6 @@ module KerPair = struct end module SyntacticOrd = struct - type t = kernel_pair let compare x y = match x, y with | Same knx, Same kny -> KerName.compare knx kny | Dual (knux,kncx), Dual (knuy,kncy) -> @@ -865,7 +864,6 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c module SyntacticOrd = struct - type t = constant * bool let compare (c, b) (c', b') = if b = b' then Constant.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e95cf4d1c..c8ac7df5c 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -61,3 +61,6 @@ val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds val dump_universes : (constraint_type -> string -> string -> unit) -> universes -> unit + +(** {6 Debugging} *) +val check_universes_invariants : universes -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index 09f884ecd..afe9cbe8d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -440,10 +440,6 @@ struct let set = make Level.set let type1 = hcons (Level.set, 1) - let is_prop = function - | (l,0) -> Level.is_prop l - | _ -> false - let is_small = function | (l,0) -> Level.is_small l | _ -> false diff --git a/lib/feedback.ml b/lib/feedback.ml index df6fe3a62..0846e419b 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -40,8 +40,6 @@ type feedback = { contents : feedback_content; } -let default_route = 0 - (** Feeders *) let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7 diff --git a/lib/stateid.ml b/lib/stateid.ml index ae25735c5..c153f0e80 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -32,7 +32,6 @@ let compare = Int.compare module Self = struct type t = int let compare = compare - let equal = equal end module Set = Set.Make(Self) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index f25b394f0..18942ac29 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -114,9 +114,6 @@ module Error = struct | UnsupportedUnicode x -> Printf.sprintf "Unsupported Unicode character (0x%x)" x) - (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) - end open Error @@ -153,10 +150,6 @@ let bump_loc_line_last loc bol_pos = in Ploc.encl loc loc' -let set_loc_file loc fname = - Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc) - (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) - (* For some reason, the [Ploc.after] function of Camlp5 does not update line numbers, so we define our own function that does it. *) let after loc = @@ -434,7 +427,6 @@ let push_char c = real_push_char c let push_string s = Buffer.add_string current_comment s -let push_bytes s = Buffer.add_bytes current_comment s let null_comment s = let rec null i = diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 496b20002..65e99d1b9 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -80,10 +80,6 @@ let create_pos = function | None -> Extend.First | Some lev -> Extend.After (constr_level lev) -type gram_level = - gram_position option * gram_assoc option * string option * - (** for reinitialization: *) gram_reinit option - let find_position_gen current ensure assoc lev = match lev with | None -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 011565d86..3438635cf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -756,11 +756,6 @@ GEXTEND Gram implicit_status = MaximallyImplicit}) items ] ]; - name_or_bang: [ - [ b = OPT "!"; id = name -> - not (Option.is_empty b), id - ] - ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ [ name = name -> [(snd name, Vernacexpr.NotImplicit)] diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index dad98e2e9..3f014c4c8 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -171,7 +171,6 @@ module Symbols : sig val sopt : G.symbol -> G.symbol val snterml : G.internal_entry * string -> G.symbol val snterm : G.internal_entry -> G.symbol - val snterml_level : G.symbol -> string end = struct let stoken tok = @@ -199,10 +198,6 @@ end = struct let slist1 x = Gramext.Slist1 x let sopt x = Gramext.Sopt x - let snterml_level = function - | Gramext.Snterml (_, l) -> l - | _ -> failwith "snterml_level" - end let camlp4_verbosity silent f x = @@ -211,8 +206,6 @@ let camlp4_verbosity silent f x = f x; warning_verbose := a -let camlp4_verbose f x = camlp4_verbosity (not !Flags.quiet) f x - (** Grammar extensions *) (** NB: [extend_statment = diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8dae17d69..df81bc78c 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 *) (* diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 38fdfb759..35cfe8b54 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -52,8 +52,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/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index bcb28f77c..a853576f2 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/tacentries.ml b/plugins/ltac/tacentries.ml index 8cda73b4b..ef1d69d35 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -88,9 +88,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) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 3f83f104e..75227def0 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 50f43931e..fcdf7bb2c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -436,12 +436,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/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index b1ff59e78..41f2edfcf 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)^"]" (*********************************************************************** @@ -252,59 +251,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 +541,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 a5b016611..632b9dac1 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 *) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index dd68eac24..6e072e831 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -279,8 +279,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/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index fc7963b2d..60c199bf5 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -90,8 +90,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 +302,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 +367,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,10 +431,6 @@ 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 @@ -917,13 +904,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 +1025,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 diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 894cdb943..1f984b160 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -226,7 +226,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 diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 532cc8baa..4a3836d86 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -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 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 38eeda9b9..3041ac259 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -212,10 +212,6 @@ let tag_var = tag Tag.variable | Some (_,ExplByName id) -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" - let pr_opt_type pr = function - | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () - | t -> cut () ++ str ":" ++ pr t - let pr_opt_type_spc pr = function | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e4a87739b..58475630e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -395,10 +395,6 @@ open Decl_kinds pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) - let pr_priority = function - | None -> mt () - | Some i -> spc () ++ str "|" ++ spc () ++ int i - (**************************************) (* Pretty printer for vernac commands *) (**************************************) diff --git a/printing/printer.ml b/printing/printer.ml index 35ddf2e8c..93d221f03 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -370,11 +370,6 @@ let pr_context_limit_compact ?n env sigma = env ~init:(mt ()) in (sign_env ++ db_env) -(* compact printing an env (variables and de Bruijn). Separator: three - spaces between simple hyps, and newline otherwise *) -let pr_context_unlimited_compact env sigma = - pr_context_limit_compact env sigma - (* The number of printed hypothesis in a goal *) (* If [None], no limit *) let print_hyps_limit = ref (None : int option) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f9ebc4233..605914a01 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -27,11 +27,6 @@ open Unification open Misctypes open Sigma.Notations -(* Abbreviations *) - -let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c - (******************************************************************) (* Clausal environments *) diff --git a/proofs/logic.ml b/proofs/logic.ml index e6024785d..9ab8c34d8 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -97,11 +97,6 @@ let check_typability env sigma c = (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) -let clear_hyps env sigma ids sign cl = - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in - (hyps, cl, !evdref) - let clear_hyps2 env sigma ids sign t cl = let evdref = ref (Evd.clear_metas sigma) in let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b55f8ef11..97c5cda77 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -179,9 +179,6 @@ module New = struct let pf_unsafe_type_of gl t = pf_apply unsafe_type_of gl t - let pf_get_type_of gl t = - pf_apply (Retyping.get_type_of ~lax:true) gl t - let pf_type_of gl t = pf_apply type_of gl t diff --git a/stm/stm.ml b/stm/stm.ml index 3738aa94a..f773d60c5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1041,13 +1041,6 @@ end = struct (* {{{ *) | `Stop x -> x | `Cont acc -> next acc - let back_safe () = - let id = - fold_until (fun n (id,_,_,_,_) -> - if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n)) - 0 (VCS.get_branch_pos (VCS.current_branch ())) in - backto id - let undo_vernac_classifier v = try match v with diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 851554b83..15b40b42d 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 let meta3 = mkmeta 3 -let meta4 = mkmeta 4 let op2bool = function Some _ -> true | None -> false diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9c2a1d850..53f8e4d5f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5039,8 +5039,6 @@ end module New = struct open Proofview.Notations - let exact_proof c = exact_proof c - open Genredexpr open Locus diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 853bc29aa..235f2588c 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -64,7 +64,6 @@ val keyword : string -> loc -> unit val ident : string -> loc option -> unit val sublexer : char -> loc -> unit val sublexer_in_doc : char -> unit -val initialize : unit -> unit val proofbox : unit -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 48cd70f69..9f6f77ef1 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -41,7 +41,6 @@ let vernac_echo loc in_chan = let open Loc in (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) -let chan_beautify = ref stdout let beautify_suffix = ".beautified" let set_formatter_translator ch = diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index b9c4c6cc5..015552d68 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -28,8 +28,6 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration -let out_punivs = Univ.out_punivs - (**********************************************************************) (* Generic synthesis of boolean equality *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f86a0ef92..bb5be4cb0 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -527,7 +527,7 @@ let warn_skip_spaces_curly = (fun () ->strbrk "Skipping spaces inside curly brackets") let rec drop_spacing = function - | UnpCut _ as u :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt + | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt | fmt -> fmt diff --git a/vernac/record.ml b/vernac/record.ml index 8b4b7606f..53722b8f6 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -216,7 +216,7 @@ let warning_or_error coe indsp err = (pr_id fi ++ strbrk " cannot be defined because it is not typable.") in if coe then user_err ~hdr:"structure" st; - Flags.if_verbose Feedback.msg_info (hov 0 st) + warn_cannot_define_projection (hov 0 st) type field_status = | NoProjection of Name.t diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index a1835959c..e44b585d7 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -106,8 +106,6 @@ module Tag = struct end -type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit - let msgnl_with ?pre_hdr fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () @@ -283,16 +281,6 @@ let print_err_exn ?extra any = let msg = CErrors.iprint (e, info) ++ fnl () in std_logger ~pre_hdr Feedback.Error msg -(* Output to file, used only in extraction so a candidate for removal *) -let ft_logger old_logger ft ?loc level mesg = - let id x = x in - match level with - | Debug -> msgnl_with ft (make_body id dbg_hdr mesg) - | Info -> msgnl_with ft (make_body id info_hdr mesg) - | Notice -> msgnl_with ft mesg - | Warning -> old_logger ?loc level mesg - | Error -> old_logger ?loc level mesg - let with_output_to_file fname func input = (* XXX FIXME: redirect std_ft *) (* let old_logger = !logger in *) -- cgit v1.2.3 From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Thu, 27 Apr 2017 21:58:52 +0200 Subject: Post-rebase warnings (unused opens and 2 unused values) --- plugins/cc/cctac.ml | 2 -- plugins/cc/cctac.mli | 1 - plugins/firstorder/formula.ml | 1 - plugins/firstorder/instances.ml | 1 - plugins/firstorder/rules.ml | 1 - plugins/firstorder/rules.mli | 1 - plugins/firstorder/sequent.ml | 1 - plugins/firstorder/sequent.mli | 2 -- plugins/ltac/g_rewrite.ml4 | 1 - plugins/ltac/rewrite.ml | 1 - pretyping/constr_matching.ml | 1 - tactics/auto.ml | 3 --- tactics/class_tactics.ml | 1 - tactics/class_tactics.mli | 1 - vernac/topfmt.ml | 1 - 15 files changed, 19 deletions(-) (limited to 'vernac/topfmt.ml') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 00b31ccce..7c5efaea3 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 5099d847b..b4bb62be8 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/firstorder/formula.ml b/plugins/firstorder/formula.ml index ade94e98e..9900792ca 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/instances.ml b/plugins/firstorder/instances.ml index 2b624b983..5a1e7c26a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -10,7 +10,6 @@ open Unify open Rules open CErrors open Util -open Term open EConstr open Vars open Tacmach.New diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index e0d2c38a7..86a677007 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 80a7ae2c2..fb2173083 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 59b842c82..2d18b6605 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 18d68f54f..6ed251f34 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/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index fdcaedab3..ac979bcf8 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/rewrite.ml b/plugins/ltac/rewrite.ml index 9a1615d3f..5630a2d7b 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 diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index d55350622..2334be966 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/tactics/auto.ml b/tactics/auto.ml index 324c551d0..c2d12ebd0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,15 +10,12 @@ module CVars = Vars open Pp open Util -open CErrors open Names open Termops open EConstr open Environ -open Tacmach open Genredexpr open Tactics -open Tacticals open Clenv open Locus open Proofview.Notations diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6c724a1eb..2d6dffdd2 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -19,7 +19,6 @@ open Term open Termops open EConstr open Proof_type -open Tacticals open Tacmach open Tactics open Clenv diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 4ab29f260..c5731e377 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Tacmach val catchable : exn -> bool diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index e44b585d7..6d9d71a62 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -131,7 +131,6 @@ let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc () let info_hdr = mt () let warn_hdr = tag Tag.warning (str "Warning:") ++ spc () let err_hdr = tag Tag.error (str "Error:") ++ spc () -let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc () let make_body quoter info ?pre_hdr s = pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s)) -- cgit v1.2.3