diff options
191 files changed, 448 insertions, 1121 deletions
@@ -1,4 +1,4 @@ -FLG -rectypes -thread -safe-string +FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50 S ltac B ltac diff --git a/checker/checker.ml b/checker/checker.ml index 95a9ea78b..5cadfe7b9 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -221,7 +221,7 @@ let where = function | Some s -> if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) -let rec explain_exn = function +let explain_exn = function | Stream.Failure -> hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> @@ -354,7 +354,7 @@ let parse_args argv = | "-norec" :: [] -> usage () | "-silent" :: rem -> - Flags.make_silent true; parse rem + Flags.quiet := true; parse rem | s :: _ when s<>"" && s.[0]='-' -> fatal_error (str "Unknown option " ++ str s) false 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 1fe02c8b6..ad93146d5 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -6,6 +6,7 @@ open Term (** Substitutions, code imported from kernel/mod_subst *) module Deltamap = struct + [@@@ocaml.warning "-32-34"] type t = delta_resolver let empty = MPmap.empty, KNmap.empty let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km @@ -25,6 +26,7 @@ end let empty_delta_resolver = Deltamap.empty module Umap = struct + [@@@ocaml.warning "-32-34"] type 'a t = 'a umap_t let empty = MPmap.empty, MBImap.empty let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 @@ -461,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 @@ -515,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/include b/checker/include index 6bea3c91a..09bf2826c 100644 --- a/checker/include +++ b/checker/include @@ -116,7 +116,7 @@ let prsub s = #install_printer prsub;;*) Checker.init_with_argv [|"";"-coqlib";"."|];; -Flags.make_silent false;; +Flags.quiet := false;; Flags.debug := true;; Sys.catch_break true;; diff --git a/checker/inductive.ml b/checker/inductive.ml index c4ffc141f..8f23a38af 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -149,7 +149,7 @@ let remember_subst u subst = (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = +let make_subst env = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) @@ -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/configure.ml b/configure.ml index befd67262..5330da7d3 100644 --- a/configure.ml +++ b/configure.ml @@ -270,6 +270,7 @@ module Prefs = struct let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" let force_caml_version = ref false + let warn_error = ref false end (* TODO : earlier any option -foo was also available as --foo *) @@ -352,6 +353,8 @@ let args_options = Arg.align [ " URL of the coq website"; "-force-caml-version", Arg.Set Prefs.force_caml_version, " Force OCaml version"; + "-warn-error", Arg.Set Prefs.warn_error, + " Make OCaml warnings into errors"; ] let parse_args () = @@ -511,6 +514,32 @@ let camltag = match caml_version_list with | x::y::_ -> "OCAML"^x^y | _ -> assert false +(** Explanation of disabled warnings: + 3: deprecated warning (not error for non minimum supported ocaml) + 4: fragile pattern matching: too common in the code and too annoying to avoid in general + 9: missing fields in a record pattern: too common in the code and not worth the bother + 27: innocuous unused variable: innocuous + 41: ambiguous constructor or label: too common + 42: disambiguated counstructor or label: too common + 44: "open" shadowing already defined identifier: too common, especially when some are aliases + 45: "open" shadowing a label or constructor: see 44 + 48: implicit elimination of optional arguments: too common + 50: unexpected documentation comment: too common and annoying to avoid + 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 +*) +let coq_warn_flags = + let warnings = "-w +a-4-9-27-41-42-44-45-48-50" in + let errors = + if !Prefs.warn_error + then "-warn-error +a" + ^ (if caml_version_nums > [4;2;3] + then "-3-56" + else "") + else "" + in + warnings ^ " " ^ errors + + (** * CamlpX configuration *) @@ -1103,7 +1132,7 @@ let write_makefile f = pr "CAMLHLIB=%S\n\n" camllib; pr "# Caml link command and Caml make top command\n"; pr "# Caml flags\n"; - pr "CAMLFLAGS=-rectypes %s %s\n" coq_annotate_flag coq_safe_string; + pr "CAMLFLAGS=-rectypes %s %s %s\n" coq_warn_flags coq_annotate_flag coq_safe_string; pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; pr "# Flags for GCC\n"; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 474cc85c1..7caaf2d9d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -7,6 +7,7 @@ (************************************************************************) (* Printers for the ocaml toplevel. *) +[@@@ocaml.warning "-32"] open Util open Pp @@ -502,7 +503,6 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Pcoq open Genarg open Stdarg open Egramml diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bb9075e74..54d3ce6cf 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CSig open CErrors open Util open Names diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3a9469e55..693b592fd 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -9,7 +9,6 @@ open CSig open Names open Constr -open Context open Environ type t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 22f93faa6..e85c1f6fd 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -10,7 +10,6 @@ open CErrors open Util open Names open Term -open Vars open Termops open Namegen open Pre_env diff --git a/engine/evd.ml b/engine/evd.ml index 5419a10a8..db048bbd6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -14,10 +14,8 @@ open Nameops open Term open Vars open Environ -open Globnames -open Context.Named.Declaration -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) module NamedDecl = Context.Named.Declaration (** Generic filters *) @@ -360,8 +358,6 @@ module EvMap = Evar.Map module EvNames : sig -open Misctypes - type t val empty : t diff --git a/engine/proofview.mli b/engine/proofview.mli index a3b0304b1..da8a8fecd 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -13,7 +13,6 @@ state and returning a value of type ['a]. *) open Util -open Term open EConstr (** Main state of tactics *) diff --git a/engine/termops.ml b/engine/termops.ml index 64f4c6dc5..19e62f8e6 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 @@ -1451,7 +1427,6 @@ let dependency_closure env sigma sign hyps = List.rev lh let global_app_of_constr sigma c = - let open Univ in let open Globnames in match EConstr.kind sigma c with | Const (c, u) -> (ConstRef c, u), None diff --git a/engine/universes.ml b/engine/universes.ml index ad5ff827b..1900112dd 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -13,7 +13,6 @@ open Term open Environ open Univ open Globnames -open Decl_kinds let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) @@ -732,7 +731,7 @@ let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cs type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t -let pr_constraints_map cmap = +let _pr_constraints_map (cmap:constraints_map) = LMap.fold (fun l cstrs acc -> Level.pr l ++ str " => " ++ prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 1dd8da12a..b14fba975 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -129,7 +129,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let gl = mlexpr_of_clause clause in let level = mlexpr_of_int level in - let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in declare_str_items loc [ <:str_item< do { Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$); diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 222b9eed9..b180aa556 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -117,7 +117,7 @@ end = struct (b#get_iter_at_mark s.start)#offset (b#get_iter_at_mark s.stop)#offset (ellipsize - ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop))) + ((b#get_iter_at_mark s.start)#get_slice ~stop:(b#get_iter_at_mark s.stop))) (String.concat "," (List.map str_of_flag s.flags)) (ellipsize (String.concat "," @@ -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) @@ -207,7 +204,7 @@ object (self) in List.iter (fun s -> set_index s (s.index + 1)) after; set_index s (document_length - List.length after); - ignore ((SentenceId.connect s)#changed self#on_changed); + ignore ((SentenceId.connect s)#changed ~callback:self#on_changed); document_length <- document_length + 1; List.iter (fun f -> f `INSERT) cbs @@ -221,8 +218,8 @@ object (self) List.iter (fun f -> f `REMOVE) cbs initializer - let _ = (Doc.connect doc)#pushed self#on_push in - let _ = (Doc.connect doc)#popped self#on_pop in + let _ = (Doc.connect doc)#pushed ~callback:self#on_push in + let _ = (Doc.connect doc)#popped ~callback:self#on_pop in () end @@ -273,15 +270,15 @@ object(self) else iter in let iter = sentence_start iter in - script#buffer#place_cursor iter; + script#buffer#place_cursor ~where:iter; ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) in - let _ = segment#connect#clicked on_click in + let _ = segment#connect#clicked ~callback:on_click in () method private tooltip_callback ~x ~y ~kbd tooltip = - let x, y = script#window_to_buffer_coords `WIDGET x y in - let iter = script#get_iter_at_location x y in + let x, y = script#window_to_buffer_coords ~tag:`WIDGET ~x ~y in + let iter = script#get_iter_at_location ~x ~y in if iter#has_tag Tags.Script.tooltip then begin let s = let rec aux iter = diff --git a/ide/coqide.ml b/ide/coqide.ml index 25858acce..0b7567a5a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -792,11 +792,11 @@ let coqtop_arguments sn = sn.messages#push Feedback.Error (Pp.str msg) else dialog#destroy () in - let _ = entry#connect#activate ok_cb in - let _ = ok#connect#clicked ok_cb in + let _ = entry#connect#activate ~callback:ok_cb in + let _ = ok#connect#clicked ~callback:ok_cb in let cancel = GButton.button ~stock:`CANCEL ~packing:box#add () in let cancel_cb () = dialog#destroy () in - let _ = cancel#connect#clicked cancel_cb in + let _ = cancel#connect#clicked ~callback:cancel_cb in dialog#show () let coqtop_arguments = cb_on_current_term coqtop_arguments @@ -1274,8 +1274,8 @@ let build_ui () = if b then toolbar#misc#show () else toolbar#misc#hide () in stick show_toolbar toolbar refresh_toolbar; - let _ = source_style#connect#changed refresh_style in - let _ = source_language#connect#changed refresh_language in + let _ = source_style#connect#changed ~callback:refresh_style in + let _ = source_language#connect#changed ~callback:refresh_language in (* Color configuration *) Tags.Script.incomplete#set_property diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 2ae18593a..91c281c8d 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -28,148 +28,148 @@ let list_queries menu li = res_buf let init () = - let theui = Printf.sprintf "<ui> -<menubar name='CoqIde MenuBar'> - <menu action='File'> - <menuitem action='New' /> - <menuitem action='Open' /> - <menuitem action='Save' /> - <menuitem action='Save as' /> - <menuitem action='Save all' /> - <menuitem action='Revert all buffers' /> - <menuitem action='Close buffer' /> - <menuitem action='Print...' /> - <menu action='Export to'> - <menuitem action='Html' /> - <menuitem action='Latex' /> - <menuitem action='Dvi' /> - <menuitem action='Pdf' /> - <menuitem action='Ps' /> - </menu> - <menuitem action='Rehighlight' /> - %s - </menu> - <menu name='Edit' action='Edit'> - <menuitem action='Undo' /> - <menuitem action='Redo' /> - <separator /> - <menuitem action='Cut' /> - <menuitem action='Copy' /> - <menuitem action='Paste' /> - <separator /> - <menuitem action='Find' /> - <menuitem action='Find Next' /> - <menuitem action='Find Previous' /> - <menuitem action='Complete Word' /> - <separator /> - <menuitem action='External editor' /> - <separator /> - <menuitem name='Prefs' action='Preferences' /> - </menu> - <menu name='View' action='View'> - <menuitem action='Previous tab' /> - <menuitem action='Next tab' /> - <separator/> - <menuitem action='Zoom in' /> - <menuitem action='Zoom out' /> - <menuitem action='Zoom fit' /> - <separator/> - <menuitem action='Show Toolbar' /> - <menuitem action='Query Pane' /> - <separator/> - <menuitem action='Display implicit arguments' /> - <menuitem action='Display coercions' /> - <menuitem action='Display raw matching expressions' /> - <menuitem action='Display notations' /> - <menuitem action='Display all basic low-level contents' /> - <menuitem action='Display existential variable instances' /> - <menuitem action='Display universe levels' /> - <menuitem action='Display all low-level contents' /> - </menu> - <menu action='Navigation'> - <menuitem action='Forward' /> - <menuitem action='Backward' /> - <menuitem action='Go to' /> - <menuitem action='Start' /> - <menuitem action='End' /> - <menuitem action='Interrupt' /> - <menuitem action='Previous' /> - <menuitem action='Next' /> - </menu> - <menu action='Try Tactics'> - <menuitem action='auto' /> - <menuitem action='auto with *' /> - <menuitem action='eauto' /> - <menuitem action='eauto with *' /> - <menuitem action='intuition' /> - <menuitem action='omega' /> - <menuitem action='simpl' /> - <menuitem action='tauto' /> - <menuitem action='trivial' /> - <menuitem action='Wizard' /> - <separator /> - %s - </menu> - <menu action='Templates'> - <menuitem action='Lemma' /> - <menuitem action='Theorem' /> - <menuitem action='Definition' /> - <menuitem action='Inductive' /> - <menuitem action='Fixpoint' /> - <menuitem action='Scheme' /> - <menuitem action='match' /> - <separator /> - %s - </menu> - <menu action='Queries'> - <menuitem action='Search' /> - <menuitem action='Check' /> - <menuitem action='Print' /> - <menuitem action='About' /> - <menuitem action='Locate' /> - <menuitem action='Print Assumptions' /> - <separator /> - %s - </menu> - <menu name='Tools' action='Tools'> - <menuitem action='Comment' /> - <menuitem action='Uncomment' /> - <separator /> - <menuitem action='Coqtop arguments' /> - </menu> - <menu action='Compile'> - <menuitem action='Compile buffer' /> - <menuitem action='Make' /> - <menuitem action='Next error' /> - <menuitem action='Make makefile' /> - </menu> - <menu action='Windows'> - <menuitem action='Detach View' /> - </menu> - <menu name='Help' action='Help'> - <menuitem action='Browse Coq Manual' /> - <menuitem action='Browse Coq Library' /> - <menuitem action='Help for keyword' /> - <menuitem action='Help for μPG mode' /> - <separator /> - <menuitem name='Abt' action='About Coq' /> - </menu> -</menubar> -<toolbar name='CoqIde ToolBar'> - <toolitem action='Save' /> - <toolitem action='Close buffer' /> - <toolitem action='Forward' /> - <toolitem action='Backward' /> - <toolitem action='Go to' /> - <toolitem action='Start' /> - <toolitem action='End' /> - <toolitem action='Force' /> - <toolitem action='Interrupt' /> - <toolitem action='Previous' /> - <toolitem action='Next' /> - <toolitem action='Wizard' /> -</toolbar> -</ui>" + let theui = Printf.sprintf "<ui>\ +\n<menubar name='CoqIde MenuBar'>\ +\n <menu action='File'>\ +\n <menuitem action='New' />\ +\n <menuitem action='Open' />\ +\n <menuitem action='Save' />\ +\n <menuitem action='Save as' />\ +\n <menuitem action='Save all' />\ +\n <menuitem action='Revert all buffers' />\ +\n <menuitem action='Close buffer' />\ +\n <menuitem action='Print...' />\ +\n <menu action='Export to'>\ +\n <menuitem action='Html' />\ +\n <menuitem action='Latex' />\ +\n <menuitem action='Dvi' />\ +\n <menuitem action='Pdf' />\ +\n <menuitem action='Ps' />\ +\n </menu>\ +\n <menuitem action='Rehighlight' />\ +\n %s\ +\n </menu>\ +\n <menu name='Edit' action='Edit'>\ +\n <menuitem action='Undo' />\ +\n <menuitem action='Redo' />\ +\n <separator />\ +\n <menuitem action='Cut' />\ +\n <menuitem action='Copy' />\ +\n <menuitem action='Paste' />\ +\n <separator />\ +\n <menuitem action='Find' />\ +\n <menuitem action='Find Next' />\ +\n <menuitem action='Find Previous' />\ +\n <menuitem action='Complete Word' />\ +\n <separator />\ +\n <menuitem action='External editor' />\ +\n <separator />\ +\n <menuitem name='Prefs' action='Preferences' />\ +\n </menu>\ +\n <menu name='View' action='View'>\ +\n <menuitem action='Previous tab' />\ +\n <menuitem action='Next tab' />\ +\n <separator/>\ +\n <menuitem action='Zoom in' />\ +\n <menuitem action='Zoom out' />\ +\n <menuitem action='Zoom fit' />\ +\n <separator/>\ +\n <menuitem action='Show Toolbar' />\ +\n <menuitem action='Query Pane' />\ +\n <separator/>\ +\n <menuitem action='Display implicit arguments' />\ +\n <menuitem action='Display coercions' />\ +\n <menuitem action='Display raw matching expressions' />\ +\n <menuitem action='Display notations' />\ +\n <menuitem action='Display all basic low-level contents' />\ +\n <menuitem action='Display existential variable instances' />\ +\n <menuitem action='Display universe levels' />\ +\n <menuitem action='Display all low-level contents' />\ +\n </menu>\ +\n <menu action='Navigation'>\ +\n <menuitem action='Forward' />\ +\n <menuitem action='Backward' />\ +\n <menuitem action='Go to' />\ +\n <menuitem action='Start' />\ +\n <menuitem action='End' />\ +\n <menuitem action='Interrupt' />\ +\n <menuitem action='Previous' />\ +\n <menuitem action='Next' />\ +\n </menu>\ +\n <menu action='Try Tactics'>\ +\n <menuitem action='auto' />\ +\n <menuitem action='auto with *' />\ +\n <menuitem action='eauto' />\ +\n <menuitem action='eauto with *' />\ +\n <menuitem action='intuition' />\ +\n <menuitem action='omega' />\ +\n <menuitem action='simpl' />\ +\n <menuitem action='tauto' />\ +\n <menuitem action='trivial' />\ +\n <menuitem action='Wizard' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu action='Templates'>\ +\n <menuitem action='Lemma' />\ +\n <menuitem action='Theorem' />\ +\n <menuitem action='Definition' />\ +\n <menuitem action='Inductive' />\ +\n <menuitem action='Fixpoint' />\ +\n <menuitem action='Scheme' />\ +\n <menuitem action='match' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu action='Queries'>\ +\n <menuitem action='Search' />\ +\n <menuitem action='Check' />\ +\n <menuitem action='Print' />\ +\n <menuitem action='About' />\ +\n <menuitem action='Locate' />\ +\n <menuitem action='Print Assumptions' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu name='Tools' action='Tools'>\ +\n <menuitem action='Comment' />\ +\n <menuitem action='Uncomment' />\ +\n <separator />\ +\n <menuitem action='Coqtop arguments' />\ +\n </menu>\ +\n <menu action='Compile'>\ +\n <menuitem action='Compile buffer' />\ +\n <menuitem action='Make' />\ +\n <menuitem action='Next error' />\ +\n <menuitem action='Make makefile' />\ +\n </menu>\ +\n <menu action='Windows'>\ +\n <menuitem action='Detach View' />\ +\n </menu>\ +\n <menu name='Help' action='Help'>\ +\n <menuitem action='Browse Coq Manual' />\ +\n <menuitem action='Browse Coq Library' />\ +\n <menuitem action='Help for keyword' />\ +\n <menuitem action='Help for μPG mode' />\ +\n <separator />\ +\n <menuitem name='Abt' action='About Coq' />\ +\n </menu>\ +\n</menubar>\ +\n<toolbar name='CoqIde ToolBar'>\ +\n <toolitem action='Save' />\ +\n <toolitem action='Close buffer' />\ +\n <toolitem action='Forward' />\ +\n <toolitem action='Backward' />\ +\n <toolitem action='Go to' />\ +\n <toolitem action='Start' />\ +\n <toolitem action='End' />\ +\n <toolitem action='Force' />\ +\n <toolitem action='Interrupt' />\ +\n <toolitem action='Previous' />\ +\n <toolitem action='Next' />\ +\n <toolitem action='Wizard' />\ +\n</toolbar>\ +\n</ui>" (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") (Buffer.contents (list_items "Tactic" Coq_commands.tactics)) (Buffer.contents (list_items "Template" Coq_commands.commands)) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bf86db08f..966a94da9 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -82,7 +82,7 @@ let add ((s,eid),(sid,verbose)) = let loc_ast = Stm.parse_sentence sid pa in let newid, rc = Stm.add ~ontop:sid verbose loc_ast in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - ide_cmd_checks newid loc_ast; + ide_cmd_checks ~id:newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. * @@ -505,12 +505,12 @@ let rec parse = function let () = Coqtop.toploop_init := (fun args -> let args = parse args in - Flags.make_silent true; + Flags.quiet := true; CoqworkmgrApi.(init Flags.High); args) let () = Coqtop.toploop_run := loop let () = Usage.add_to_usage "coqidetop" -" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format - --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" +" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ +\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" diff --git a/ide/ideutils.ml b/ide/ideutils.ml index da867e689..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 @@ -58,7 +47,7 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in let start = buf#get_iter_at_mark mark in let stop = buf#get_iter_at_mark rmark in - let iter tag = buf#apply_tag tag start stop in + let iter tag = buf#apply_tag tag ~start ~stop in List.iter iter tags let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = diff --git a/ide/preferences.ml b/ide/preferences.ml index f0fd45d77..9fe9c6337 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -73,8 +73,8 @@ end let stick (pref : 'a preference) (obj : #GObj.widget as 'obj) (cb : 'a -> unit) = let _ = cb pref#get in - let p_id = pref#connect#changed (fun v -> cb v) in - let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in + let p_id = pref#connect#changed ~callback:(fun v -> cb v) in + let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in () (** Useful marshallers *) @@ -314,7 +314,7 @@ let attach_modifiers (pref : string preference) prefix = in GtkData.AccelMap.foreach change in - pref#connect#changed cb + pref#connect#changed ~callback:cb let modifier_for_navigation = new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string) @@ -360,7 +360,7 @@ object ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string) as super - method set v = + method! set v = if not (Flags.is_standard_doc_url v) && v <> use_default_doc_url && (* Extra hack to support links to last released doc version *) @@ -408,10 +408,10 @@ let background_color = new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string) let attach_bg (pref : string preference) (tag : GText.tag) = - pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c)) + pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c)) let attach_fg (pref : string preference) (tag : GText.tag) = - pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c)) + pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c)) let processing_color = new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string) @@ -468,7 +468,7 @@ let create_tag name default = let iter table = let tag = GText.tag ~name () in table#add tag#as_tag; - ignore (pref#connect#changed (fun _ -> set_tag tag)); + ignore (pref#connect#changed ~callback:(fun _ -> set_tag tag)); set_tag tag; in List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table]; @@ -601,8 +601,8 @@ object (self) box#pack italic#coerce; box#pack underline#coerce; let cb but obj = obj#set_sensitive (not but#active) in - let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in - let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in + let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in + let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in () end @@ -692,7 +692,7 @@ let configure ?(apply=(fun () -> ())) () = ~color:(Tags.color_of_string pref#get) ~packing:(table#attach ~left:1 ~top:i) () in - let _ = button#connect#color_set begin fun () -> + let _ = button#connect#color_set ~callback:begin fun () -> pref#set (Tags.string_of_color button#color) end in let reset _ = @@ -754,7 +754,7 @@ let configure ?(apply=(fun () -> ())) () = let button text (pref : bool preference) = let active = pref#get in let but = GButton.check_button ~label:text ~active ~packing:box#pack () in - ignore (but#connect#toggled (fun () -> pref#set but#active)) + ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active)) in let () = button "Dynamic word wrap" dynamic_word_wrap in let () = button "Show line number" show_line_number in diff --git a/ide/session.ml b/ide/session.ml index 6262820e7..7aea75ac8 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -249,8 +249,8 @@ let make_table_widget ?sort cd cb = let () = data#set_headers_visible true in let () = data#set_headers_clickable true in let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed refresh in - let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in + let _ = background_color#connect#changed ~callback:refresh in + let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in let mk_rend c = GTree.cell_renderer_text [], ["text",c] in let cols = List.map2 (fun (_,c) (_,n,v) -> @@ -308,8 +308,8 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = !callback errs; List.iter (fun (lno, msg) -> access (fun columns store -> let line = store#append () in - store#set line (find_int_col "Line" columns) lno; - store#set line (find_string_col "Error message" columns) msg)) + store#set ~row:line ~column:(find_int_col "Line" columns) lno; + store#set ~row:line ~column:(find_string_col "Error message" columns) msg)) errs end method on_update ~callback:cb = callback := cb @@ -348,8 +348,8 @@ let create_jobpage coqtop coqops : jobpage = else false) else let line = store#append () in - store#set line column id; - store#set line (find_string_col "Job name" columns) job)) + store#set ~row:line ~column id; + store#set ~row:line ~column:(find_string_col "Job name" columns) job)) jobs end method on_update ~callback:cb = callback := cb diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 3fcb7ce49..621c46b94 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -91,8 +91,8 @@ object(self) let result = GText.view ~packing:r_bin#add () in views <- (frame#coerce, result, combo#entry) :: views; let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = result#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in stick text_font result cb; result#misc#set_can_focus true; (* false causes problems for selection *) @@ -165,7 +165,7 @@ object(self) self#new_page_maker; self#new_query_aux ~grab_now:false (); frame#misc#hide (); - let _ = background_color#connect#changed self#refresh_color in + let _ = background_color#connect#changed ~callback:self#refresh_color in self#refresh_color background_color#get; ignore(notebook#event#connect#key_press ~callback:(fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true) diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index aeae3e1fd..3bb6b780e 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -154,7 +154,7 @@ object (self) let () = store#clear () in let iter prop = let iter = store#append () in - store#set iter column prop + store#set ~row:iter ~column prop in let () = current_completion <- (pref, props) in Proposals.iter iter props @@ -267,7 +267,7 @@ object (self) (** Position of view w.r.t. window *) let (ux, uy) = Gdk.Window.get_position view#misc#window in (** Relative buffer position to view *) - let (dx, dy) = view#window_to_buffer_coords `WIDGET 0 0 in + let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in (** Iter position *) let iter = view#buffer#get_iter pos in let coords = view#get_iter_location iter in @@ -397,11 +397,11 @@ object (self) let () = self#select_first () in let () = obj#misc#show () in let () = self#manage_scrollbar () in - obj#resize 1 1 + obj#resize ~width:1 ~height:1 method private start_callback off = let (x, y, w, h) = self#coordinates (`OFFSET off) in - let () = obj#move x (y + 3 * h / 2) in + let () = obj#move ~x ~y:(y + 3 * h / 2) in () method private update_callback (off, word, props) = @@ -433,21 +433,21 @@ object (self) else false in (** Style handling *) - let _ = view#misc#connect#style_set self#refresh_style in + let _ = view#misc#connect#style_set ~callback:self#refresh_style in let _ = self#refresh_style () in let _ = data#set_resize_mode `PARENT in let _ = frame#set_resize_mode `PARENT in (** Callback to model *) - let _ = model#connect#start_completion self#start_callback in - let _ = model#connect#update_completion self#update_callback in - let _ = model#connect#end_completion self#end_callback in + let _ = model#connect#start_completion ~callback:self#start_callback in + let _ = model#connect#update_completion ~callback:self#update_callback in + let _ = model#connect#end_completion ~callback:self#end_callback in (** Popup interaction *) - let _ = view#event#connect#key_press key_cb in + let _ = view#event#connect#key_press ~callback:key_cb in (** Hiding the popup when necessary*) - let _ = view#misc#connect#hide obj#misc#hide in - let _ = view#event#connect#button_press (fun _ -> self#hide (); false) in - let _ = view#connect#move_cursor move_cb in - let _ = view#event#connect#focus_out (fun _ -> self#hide (); false) in + let _ = view#misc#connect#hide ~callback:obj#misc#hide in + let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in + let _ = view#connect#move_cursor ~callback:move_cb in + let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in () end diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml index 3d1b63dfa..cbc34462e 100644 --- a/ide/wg_Detachable.ml +++ b/ide/wg_Detachable.ml @@ -26,8 +26,8 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) = val mutable attached_cb = (fun _ -> ()) method child = frame#child - method add = frame#add - method pack ?from ?expand ?fill ?padding w = + method! add = frame#add + method! pack ?from ?expand ?fill ?padding w = if frame#all_children = [] then self#add w else raise (Invalid_argument "detachable#pack") diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index 3d847ddcc..f84b9063b 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -186,8 +186,8 @@ class finder name (view : GText.view) = in let find_cb = generic_cb self#hide self#find_forward in let replace_cb = generic_cb self#hide self#replace in - let _ = find_entry#event#connect#key_press find_cb in - let _ = replace_entry#event#connect#key_press replace_cb in + let _ = find_entry#event#connect#key_press ~callback:find_cb in + let _ = replace_entry#event#connect#key_press ~callback:replace_cb in (** TextView interaction *) let view_cb ev = @@ -197,7 +197,7 @@ class finder name (view : GText.view) = else false else false in - let _ = view#event#connect#key_press view_cb in + let _ = view#event#connect#key_press ~callback:view_cb in () end diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml index 08d7d1983..0e5284c2f 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.ml @@ -50,7 +50,7 @@ object(self) method pages = term_list - method remove_page index = + method! remove_page index = term_list <- Util.List.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list; super#remove_page index diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 3cbe58388..f801091cf 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -188,8 +188,8 @@ let proof_view () = let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = view#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in stick text_font view cb; @@ -226,5 +226,5 @@ let proof_view () = (* Is there a better way to connect the signal ? *) (* Can this be done in the object constructor? *) let w_cb _ = pf#refresh ~force:false in - ignore (view#misc#connect#size_allocate w_cb); + ignore (view#misc#connect#size_allocate ~callback:w_cb); pf diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 218cedb36..7430f07d4 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -301,28 +301,28 @@ object (self) ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT (* HACK: missing gtksourceview features *) - method right_margin_position = + method! right_margin_position = let prop = { Gobject.name = "right-margin-position"; conv = Gobject.Data.int; } in Gobject.get prop obj - method set_right_margin_position pos = + method! set_right_margin_position pos = let prop = { Gobject.name = "right-margin-position"; conv = Gobject.Data.int; } in Gobject.set prop obj pos - method show_right_margin = + method! show_right_margin = let prop = { Gobject.name = "show-right-margin"; conv = Gobject.Data.boolean; } in Gobject.get prop obj - method set_show_right_margin show = + method! set_show_right_margin show = let prop = { Gobject.name = "show-right-margin"; conv = Gobject.Data.boolean; @@ -460,8 +460,8 @@ object (self) let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in (** Plug on preferences *) let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = self#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in stick dynamic_word_wrap self cb; diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index dbc1740ef..d527a0d13 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -75,7 +75,7 @@ object (self) self#redraw (); end in - let _ = box#misc#connect#size_allocate cb in + let _ = box#misc#connect#size_allocate ~callback:cb in let clicked_cb ev = match model with | None -> true | Some md -> @@ -86,7 +86,7 @@ object (self) let () = clicked#call idx in true in - let _ = eventbox#event#connect#button_press clicked_cb in + let _ = eventbox#event#connect#button_press ~callback:clicked_cb in let cb show = if show then self#misc#show () else self#misc#hide () in stick show_progress_bar self cb; (** Initial pixmap *) @@ -102,7 +102,7 @@ object (self) | `SET (i, color) -> if self#misc#visible then self#fill_range color i (i + 1) in - md#changed changed_cb + md#changed ~callback:changed_cb method private fill_range color i j = match model with | None -> () diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d75487ecf..3f99a3c7c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args = | Some _, GApp (loc, GRef (loc', ref, None), arg) -> GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> - user_err ~loc (str "Notation " ++ pr_qualid qid ++ - str " cannot have a universe instance, its expanded head - does not start with a reference") + user_err ~loc (str "Notation " ++ pr_qualid qid + ++ str " cannot have a universe instance," + ++ str " its expanded head does not start with a reference") in c, projapp, args2 @@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t = let t' = locate_if_hole (loc_of_glob_constr t) na t in understand_tcc_evars env evdref ~expected_type:IsType t' -open Environ - let my_intern_constr env lvar acc c = internalize env acc false lvar c diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 758d4e650..fdd50c6a1 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -18,7 +18,6 @@ open Constrexpr open Notation_term open Pretyping open Misctypes -open Decl_kinds (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) 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/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/interp/stdarg.ml b/interp/stdarg.ml index 341ff5662..5920b0d50 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Misctypes -open Tactypes open Genarg open Geninterp diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 113fe40ba..ac40a2328 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -10,7 +10,6 @@ open Loc open Names -open Term open EConstr open Libnames open Globnames diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index c3f4c4f30..ed7b0b70d 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -106,5 +106,3 @@ let search_syntactic_definition kn = let def = out_pat pat in verbose_compat kn def v; def - -open Goptions diff --git a/intf/tactypes.mli b/intf/tactypes.mli index 02cfc44e2..ef90b911c 100644 --- a/intf/tactypes.mli +++ b/intf/tactypes.mli @@ -13,7 +13,6 @@ open Loc open Names open Constrexpr -open Glob_term open Pattern open Misctypes diff --git a/kernel/constr.ml b/kernel/constr.ml index ae58fd068..eecceb32a 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -987,28 +987,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/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/nativecode.ml b/kernel/nativecode.ml index d9659d681..ba80ff590 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -16,6 +16,8 @@ open Nativeinstr open Nativelambda open Pre_env +[@@@ocaml.warning "-32-37"] + (** This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code. *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 366f9a0a6..fcb75c661 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -16,6 +16,9 @@ open Nativeinstr module RelDecl = Context.Rel.Declaration +(* I'm not messing with this stuff. *) +[@@@ocaml.warning "-32"] + (** This file defines the lambda code generation phase of the native compiler *) exception NotClosed diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 965ed67b0..8d5f6388c 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -334,6 +334,7 @@ let l_or accu x y = if is_int x && is_int y then no_check_l_or x y else accu x y +[@@@ocaml.warning "-37"] type coq_carry = | Caccu of t | C0 of t @@ -430,7 +431,7 @@ let addmuldiv accu x y z = if is_int x && is_int y && is_int z then no_check_addmuldiv x y z else accu x y z - +[@@@ocaml.warning "-34"] type coq_bool = | Baccu of t | Btrue diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cd975ee9a..ba714ada2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -487,14 +487,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then - (let cuniv = convert_instances false u1 u2 cuniv in + (let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then - (let cuniv = convert_instances false u1 u2 cuniv in + (let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible 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/backtrace.ml b/lib/backtrace.ml index b3b8bdea2..be9f40c1f 100644 --- a/lib/backtrace.ml +++ b/lib/backtrace.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +[@@@ocaml.warning "-37"] type raw_frame = | Known_location of bool (* is_raise *) 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/lib/cWarnings.ml b/lib/cWarnings.ml index 2f569d284..71e02b3ba 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -82,7 +82,7 @@ let set_all_warnings_status status = let set_category_status ~name status = let names = Hashtbl.find categories name in - List.iter (fun name -> set_warning_status name status) names + List.iter (fun name -> set_warning_status ~name status) names let is_all_keyword name = CString.equal name "all" let is_none_keyword s = CString.equal s "none" @@ -166,7 +166,7 @@ let normalize_flags_string s = let flags = normalize_flags ~silent:false flags in string_of_flags flags -let rec parse_warnings items = +let parse_warnings items = CList.iter (fun (status, name) -> set_status ~name status) items (* For compatibility, we accept "none" *) 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/library/goptions.ml b/library/goptions.ml index 1c08b9539..c111113ca 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -235,7 +235,6 @@ with Not_found -> then error "Sorry, this option name is already used." open Libobject -open Lib let warn_deprecated_option = CWarnings.create ~name:"deprecated-option" ~category:"deprecated" diff --git a/library/libobject.ml b/library/libobject.ml index 8757ca08c..897591762 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,7 +8,6 @@ open Libnames open Pp -open Util module Dyn = Dyn.Make(struct end) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 6d259e1b1..462905808 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -99,7 +99,6 @@ module Error = struct | Unterminated_string | Undefined_token | Bad_token of string - | UnsupportedUnicode of int exception E of t @@ -110,12 +109,7 @@ module Error = struct | Unterminated_comment -> "Unterminated comment" | Unterminated_string -> "Unterminated string" | Undefined_token -> "Undefined token" - | Bad_token tok -> Format.sprintf "Bad token %S" tok - | 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)) + | Bad_token tok -> Format.sprintf "Bad token %S" tok) end open Error @@ -153,10 +147,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 = @@ -345,13 +335,13 @@ let rec string loc ~comm_level bp len = parser if esc then string loc ~comm_level bp (store len '"') s else (loc, len) | [< ''('; s >] -> (parser - | [< ''*'; s >] -> - string loc - (Option.map succ comm_level) + | [< ''*'; s >] -> + let comm_level = Option.map succ comm_level in + string loc ~comm_level bp (store (store len '(') '*') s | [< >] -> - string loc comm_level bp (store len '(') s) s + string loc ~comm_level bp (store len '(') s) s | [< ''*'; s >] -> (parser | [< '')'; s >] -> @@ -361,9 +351,9 @@ let rec string loc ~comm_level bp len = parser | _ -> () in let comm_level = Option.map pred comm_level in - string loc comm_level bp (store (store len '*') ')') s + string loc ~comm_level bp (store (store len '*') ')') s | [< >] -> - string loc comm_level bp (store len '*') s) s + string loc ~comm_level bp (store len '*') s) s | [< ''\n' as c; s >] ep -> (* If we are parsing a comment, the string if not part of a token so we update the first line of the location. Otherwise, we update the last @@ -372,8 +362,8 @@ let rec string loc ~comm_level bp len = parser if Option.has_some comm_level then bump_loc_line loc ep else bump_loc_line_last loc ep in - string loc comm_level bp (store len c) s - | [< 'c; s >] -> string loc comm_level bp (store len c) s + string loc ~comm_level bp (store len c) s + | [< 'c; s >] -> string loc ~comm_level bp (store len c) s | [< _ = Stream.empty >] ep -> let loc = set_loc_pos loc bp ep in err loc Unterminated_string @@ -434,7 +424,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 = @@ -613,7 +602,7 @@ let rec next_token loc = parser bp | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> comment_stop bp; (INT (get_buff len), set_loc_pos loc bp ep) - | [< ''\"'; (loc,len) = string loc None bp 0 >] ep -> + | [< ''\"'; (loc,len) = string loc ~comm_level:None bp 0 >] ep -> comment_stop bp; (STRING (get_buff len), set_loc_pos loc bp ep) | [< ' ('(' as c); diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 496b20002..86c66ec5f 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -10,7 +10,6 @@ open CErrors open Util open Pcoq open Constrexpr -open Notation open Notation_term open Extend open Libnames @@ -80,10 +79,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/egramcoq.mli b/parsing/egramcoq.mli index 6dda3817a..0a0430ba6 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -6,14 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Constrexpr -open Notation_term -open Pcoq -open Extend -open Genarg -open Egramml - (** Mapping of grammar productions to camlp4 actions *) (** This is the part specific to Coq-level Notation and Tactic Notation. diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 2af4ed533..abb463f82 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -8,7 +8,6 @@ open Names open Libnames -open Tok (* necessary for camlp4 *) open Pcoq open Pcoq.Prim diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 7ca2e4a4f..68b8be6b8 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -9,7 +9,6 @@ open Constrexpr open Vernacexpr open Misctypes -open Tok open Pcoq open Pcoq.Prim diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8f6b28f13..085c98e37 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..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 @@ -171,7 +170,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 +197,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 +205,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/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/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 2b12462ad..322fbcea7 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -657,7 +657,7 @@ let extraction_library is_rec m = let l = List.rev (environment_until (Some dir_m)) in let select l (mp,struc) = if Visit.needed_mp mp - then (mp, extract_structure env mp no_delta true struc) :: l + then (mp, extract_structure env mp no_delta ~all:true struc) :: l else l in let struc = List.fold_left select [] l in 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/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/firstorder/instances.ml b/plugins/firstorder/instances.ml index 62f811546..5a1e7c26a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -10,14 +10,12 @@ open Unify open Rules open CErrors open Util -open Term open EConstr open Vars open Tacmach.New open Tactics open Tacticals.New open Proofview.Notations -open Termops open Reductionops open Formula open Sequent 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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8dae17d69..55d361e3d 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 *) (* @@ -235,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 @@ -542,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/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 7ddc84d01..61752aa33 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -1,5 +1,4 @@ open Names -open Term val prove_princ_for_struct : Evd.evar_map ref -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 0dccd25d7..b5eacee81 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Util -open Term open Pp open Constrexpr open Indfun_common diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7b0d7d27d..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 @@ -508,7 +505,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - let open EConstr in if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; let rec lamdec_rec l n c = if Int.equal n 0 then l,c diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 94ec0a898..6c0c28905 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -7,7 +7,6 @@ (************************************************************************) open Ltac_plugin -open Tacexpr open Declarations open CErrors open Util @@ -1026,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 @@ -1041,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/merge.ml b/plugins/funind/merge.ml index f1ca57585..0af0898a0 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -19,7 +19,6 @@ open Pp open Names open Term open Vars -open Termops open Declarations open Glob_term open Glob_termops 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/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 5d3f6df03..bc9c300e2 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -9,7 +9,6 @@ open Util open Names open Term -open EConstr open CErrors open Evar_refiner open Tacmach diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 38fdfb759..21419d1f9 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -21,7 +21,6 @@ open Tacexpr open Glob_ops open CErrors open Util -open Evd open Termops open Equality open Misctypes @@ -52,8 +51,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/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index dfa8331ff..50e8255a6 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -16,7 +16,6 @@ open Pcoq.Constr open Pltac open Hints open Tacexpr -open Proofview.Notations open Names DECLARE PLUGIN "g_auto" diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index ff5e7d5ff..23ce368ee 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,9 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Misctypes open Class_tactics -open Pltac open Stdarg open Tacarg open Names @@ -95,7 +93,6 @@ END (** TODO: DEPRECATE *) (* A progress test that allows to see if the evars have changed *) open Term -open Proofview.Goal open Proofview.Notations let rec eq_constr_mod_evars sigma x y = 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/pltac.ml b/plugins/ltac/pltac.ml index 1d21118ae..7e979d269 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 39ae1f41d..b73b66e56 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -250,7 +250,7 @@ type 'a extra_genarg_printer = let pr_alias_key key = try let prods = (KNmap.find key !prnotation_tab).pptac_prods in - let rec pr = function + let pr = function | TacTerm s -> primitive s | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) in @@ -314,7 +314,7 @@ type 'a extra_genarg_printer = | Extend.Uentry _ | Extend.Uentryl _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" - let rec pr_targ prtac symb arg = match symb with + let pr_targ prtac symb arg = match symb with | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> prtac (1, Any) arg | Extend.Uentryl (_, l) -> prtac (l, Any) arg 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/rewrite.ml b/plugins/ltac/rewrite.ml index 12a1566e2..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 @@ -39,7 +38,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/rewrite.mli b/plugins/ltac/rewrite.mli index 7a20838a2..6683d753b 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -14,7 +14,6 @@ open Constrexpr open Tacexpr open Misctypes open Evd -open Proof_type open Tacinterp (** TODO: document and clean me! *) diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 9c4ac5265..4a44f86d9 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -8,7 +8,6 @@ open Util open Names -open Term open EConstr open Misctypes open Pattern diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index cd8c9e471..32750383b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -15,7 +15,6 @@ open Genarg open Extend open Pcoq open Egramml -open Egramcoq open Vernacexpr open Libnames open Nameops @@ -88,9 +87,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) @@ -320,7 +316,7 @@ let add_tactic_notation local n prods e = let ids = List.map_filter cons_production_parameter prods in let prods = List.map interp_prod_item prods in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in - add_glob_tactic_notation local n prods false ids tac + add_glob_tactic_notation local ~level:n prods false ids tac (**********************************************************************) (* ML Tactic entries *) diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 94e14223a..d1e2a7bbe 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Genarg open Names open Tacexpr open Geninterp 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..b8c021f18 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -25,7 +25,6 @@ open Refiner open Tacmach.New open Tactic_debug open Constrexpr -open Term open Termops open Tacexpr open Genarg @@ -436,12 +435,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/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 1e5f6bd42..494f36a95 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -8,7 +8,6 @@ open Names open Tactic_debug -open Term open EConstr open Tacexpr open Genarg diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 7745d9b7b..0b4d35a22 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -10,7 +10,6 @@ open Environ open Pattern open Names open Tacexpr -open Term open EConstr open Evd diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index dc7ee6a23..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 @@ -242,7 +241,7 @@ let tauto_uniform_unit_flags = { } (* This is the compatibility mode (not used) *) -let tauto_legacy_flags = { +let _tauto_legacy_flags = { binary_mode = true; binary_mode_bugged_detection = true; strict_in_contravariant_hyp = true; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index eb26c5431..a36607ec3 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -331,7 +331,6 @@ module M = struct open Coqlib - open Term open Constr open EConstr diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index f4f9b3c2f..377994415 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -99,7 +99,7 @@ module PSet = ISet module System = Hashtbl.Make(Vect) type proof = -| Hyp of int +| Assum of int | Elim of var * proof * proof | And of proof * proof @@ -134,7 +134,7 @@ exception SystemContradiction of proof let hyps prf = let rec hyps prf acc = match prf with - | Hyp i -> ISet.add i acc + | Assum i -> ISet.add i acc | Elim(_,prf1,prf2) | And(prf1,prf2) -> hyps prf1 (hyps prf2 acc) in hyps prf ISet.empty @@ -143,7 +143,7 @@ let hyps prf = (** Pretty printing *) let rec pp_proof o prf = match prf with - | Hyp i -> Printf.fprintf o "H%i" i + | Assum i -> Printf.fprintf o "H%i" i | Elim(v, prf1,prf2) -> Printf.fprintf o "E(%i,%a,%a)" v pp_proof prf1 pp_proof prf2 | And(prf1,prf2) -> Printf.fprintf o "A(%a,%a)" pp_proof prf1 pp_proof prf2 @@ -270,7 +270,7 @@ let norm_cstr {coeffs = v ; op = o ; cst = c} idx = (match o with | Eq -> Some c , Some c | Ge -> Some c , None) ; - prf = Hyp idx } + prf = Assum idx } (** [load_system l] takes a list of constraints of type [cstr_compat] @@ -285,7 +285,7 @@ let load_system l = let vars = List.fold_left (fun vrs (cstr,i) -> match norm_cstr cstr i with - | Contradiction -> raise (SystemContradiction (Hyp i)) + | Contradiction -> raise (SystemContradiction (Assum i)) | Redundant -> vrs | Cstr(vect,info) -> xadd_cstr vect info sys ; @@ -867,7 +867,7 @@ let mk_proof hyps prf = let rec mk_proof prf = match prf with - | Hyp i -> [ ([i, Int 1] , List.nth hyps i) ] + | Assum i -> [ ([i, Int 1] , List.nth hyps i) ] | Elim(v,prf1,prf2) -> let prfsl = mk_proof prf1 diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index cc89e2b9d..e1ceabe9e 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -21,8 +21,6 @@ let debugging = ref false;; exception Sanity;; -exception Unsolvable;; - (* ------------------------------------------------------------------------- *) (* Turn a rational into a decimal string with d sig digits. *) (* ------------------------------------------------------------------------- *) @@ -99,28 +97,11 @@ let vector_const c n = if c =/ Int 0 then vector_0 n else (n,itlist (fun k -> k |-> c) (1--n) undefined :vector);; -let vector_1 = vector_const (Int 1);; - let vector_cmul c (v:vector) = let n = dim v in if c =/ Int 0 then vector_0 n else n,mapf (fun x -> c */ x) (snd v) -let vector_neg (v:vector) = (fst v,mapf minus_num (snd v) :vector);; - -let vector_add (v1:vector) (v2:vector) = - let m = dim v1 and n = dim v2 in - if m <> n then failwith "vector_add: incompatible dimensions" else - (n,combine (+/) (fun x -> x =/ Int 0) (snd v1) (snd v2) :vector);; - -let vector_sub v1 v2 = vector_add v1 (vector_neg v2);; - -let vector_dot (v1:vector) (v2:vector) = - let m = dim v1 and n = dim v2 in - if m <> n then failwith "vector_add: incompatible dimensions" else - foldl (fun a i x -> x +/ a) (Int 0) - (combine ( */ ) (fun x -> x =/ Int 0) (snd v1) (snd v2));; - let vector_of_list l = let n = List.length l in (n,itlist2 (|->) (1--n) l undefined :vector);; @@ -133,13 +114,6 @@ let matrix_0 (m,n) = ((m,n),undefined:matrix);; let dimensions (m:matrix) = fst m;; -let matrix_const c (m,n as mn) = - if m <> n then failwith "matrix_const: needs to be square" - else if c =/ Int 0 then matrix_0 mn - else (mn,itlist (fun k -> (k,k) |-> c) (1--n) undefined :matrix);; - -let matrix_1 = matrix_const (Int 1);; - let matrix_cmul c (m:matrix) = let (i,j) = dimensions m in if c =/ Int 0 then matrix_0 (i,j) @@ -152,8 +126,6 @@ let matrix_add (m1:matrix) (m2:matrix) = if d1 <> d2 then failwith "matrix_add: incompatible dimensions" else (d1,combine (+/) (fun x -> x =/ Int 0) (snd m1) (snd m2) :matrix);; -let matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);; - let row k (m:matrix) = let i,j = dimensions m in (j, @@ -166,20 +138,10 @@ let column k (m:matrix) = foldl (fun a (i,j) c -> if j = k then (i |-> c) a else a) undefined (snd m) : vector);; -let transp (m:matrix) = - let i,j = dimensions m in - ((j,i),foldl (fun a (i,j) c -> ((j,i) |-> c) a) undefined (snd m) :matrix);; - let diagonal (v:vector) = let n = dim v in ((n,n),foldl (fun a i c -> ((i,i) |-> c) a) undefined (snd v) : matrix);; -let matrix_of_list l = - let m = List.length l in - if m = 0 then matrix_0 (0,0) else - let n = List.length (List.hd l) in - (m,n),itern 1 l (fun v i -> itern 1 v (fun c j -> (i,j) |-> c)) undefined;; - (* ------------------------------------------------------------------------- *) (* Monomials. *) (* ------------------------------------------------------------------------- *) @@ -195,24 +157,8 @@ let monomial_var x = (x |=> 1 :monomial);; let (monomial_mul:monomial->monomial->monomial) = combine (+) (fun x -> false);; -let monomial_pow (m:monomial) k = - if k = 0 then monomial_1 - else mapf (fun x -> k * x) m;; - -let monomial_divides (m1:monomial) (m2:monomial) = - foldl (fun a x k -> tryapplyd m2 x 0 >= k && a) true m1;; - -let monomial_div (m1:monomial) (m2:monomial) = - let m = combine (+) (fun x -> x = 0) m1 (mapf (fun x -> -x) m2) in - if foldl (fun a x k -> k >= 0 && a) true m then m - else failwith "monomial_div: non-divisible";; - let monomial_degree x (m:monomial) = tryapplyd m x 0;; -let monomial_lcm (m1:monomial) (m2:monomial) = - (itlist (fun x -> x |-> max (monomial_degree x m1) (monomial_degree x m2)) - (union (dom m1) (dom m2)) undefined :monomial);; - let monomial_multidegree (m:monomial) = foldl (fun a x k -> k + a) 0 m;; let monomial_variables m = dom m;; @@ -252,12 +198,6 @@ let poly_cmmul (c,m) (p:poly) = let poly_mul (p1:poly) (p2:poly) = foldl (fun a m c -> poly_add (poly_cmmul (c,m) p2) a) poly_0 p1;; -let poly_div (p1:poly) (p2:poly) = - if not(poly_isconst p2) then failwith "poly_div: non-constant" else - let c = eval undefined p2 in - if c =/ Int 0 then failwith "poly_div: division by zero" - else poly_cmul (Int 1 // c) p1;; - let poly_square p = poly_mul p p;; let rec poly_pow p k = @@ -266,10 +206,6 @@ let rec poly_pow p k = else let q = poly_square(poly_pow p (k / 2)) in if k mod 2 = 1 then poly_mul p q else q;; -let poly_exp p1 p2 = - if not(poly_isconst p2) then failwith "poly_exp: not a constant" else - poly_pow p1 (Num.int_of_num (eval undefined p2));; - let degree x (p:poly) = foldl (fun a m c -> max (monomial_degree x m) a) 0 p;; let multidegree (p:poly) = @@ -282,14 +218,14 @@ let poly_variables (p:poly) = (* Order monomials for human presentation. *) (* ------------------------------------------------------------------------- *) -let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 or x1 = x2 && k1 > k2;; +let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 || x1 = x2 && k1 > k2;; let humanorder_monomial = let rec ord l1 l2 = match (l1,l2) with _,[] -> true | [],_ -> false - | h1::t1,h2::t2 -> humanorder_varpow h1 h2 or h1 = h2 && ord t1 t2 in - fun m1 m2 -> m1 = m2 or + | h1::t1,h2::t2 -> humanorder_varpow h1 h2 || h1 = h2 && ord t1 t2 in + fun m1 m2 -> m1 = m2 || ord (sort humanorder_varpow (graph m1)) (sort humanorder_varpow (graph m2));; @@ -297,42 +233,8 @@ let humanorder_monomial = (* Conversions to strings. *) (* ------------------------------------------------------------------------- *) -let string_of_vector min_size max_size (v:vector) = - let n_raw = dim v in - if n_raw = 0 then "[]" else - let n = max min_size (min n_raw max_size) in - let xs = List.map ((o) string_of_num (element v)) (1--n) in - "[" ^ end_itlist (fun s t -> s ^ ", " ^ t) xs ^ - (if n_raw > max_size then ", ...]" else "]");; - -let string_of_matrix max_size (m:matrix) = - let i_raw,j_raw = dimensions m in - let i = min max_size i_raw and j = min max_size j_raw in - let rstr = List.map (fun k -> string_of_vector j j (row k m)) (1--i) in - "["^end_itlist(fun s t -> s^";\n "^t) rstr ^ - (if j > max_size then "\n ...]" else "]");; - let string_of_vname (v:vname): string = (v: string);; -let rec string_of_term t = - match t with - Opp t1 -> "(- " ^ string_of_term t1 ^ ")" -| Add (t1, t2) -> - "(" ^ (string_of_term t1) ^ " + " ^ (string_of_term t2) ^ ")" -| Sub (t1, t2) -> - "(" ^ (string_of_term t1) ^ " - " ^ (string_of_term t2) ^ ")" -| Mul (t1, t2) -> - "(" ^ (string_of_term t1) ^ " * " ^ (string_of_term t2) ^ ")" -| Inv t1 -> "(/ " ^ string_of_term t1 ^ ")" -| Div (t1, t2) -> - "(" ^ (string_of_term t1) ^ " / " ^ (string_of_term t2) ^ ")" -| Pow (t1, n1) -> - "(" ^ (string_of_term t1) ^ " ^ " ^ (string_of_int n1) ^ ")" -| Zero -> "0" -| Var v -> "x" ^ (string_of_vname v) -| Const x -> string_of_num x;; - - let string_of_varpow x k = if k = 1 then string_of_vname x else string_of_vname x^"^"^string_of_int k;; @@ -363,6 +265,7 @@ let string_of_poly (p:poly) = (* Printers. *) (* ------------------------------------------------------------------------- *) +(* let print_vector v = Format.print_string(string_of_vector 0 20 v);; let print_matrix m = Format.print_string(string_of_matrix 20 m);; @@ -371,7 +274,6 @@ let print_monomial m = Format.print_string(string_of_monomial m);; let print_poly m = Format.print_string(string_of_poly m);; -(* #install_printer print_vector;; #install_printer print_matrix;; #install_printer print_monomial;; @@ -411,19 +313,6 @@ let sdpa_of_vector (v:vector) = end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";; (* ------------------------------------------------------------------------- *) -(* String for block diagonal matrix numbered k. *) -(* ------------------------------------------------------------------------- *) - -let sdpa_of_blockdiagonal k m = - let pfx = string_of_int k ^" " in - let ents = - foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in - let entss = sort (increasing fst) ents in - itlist (fun ((b,i,j),c) a -> - pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ - " " ^ decimalize 20 c ^ "\n" ^ a) entss "";; - -(* ------------------------------------------------------------------------- *) (* String for a matrix numbered k, in SDPA sparse format. *) (* ------------------------------------------------------------------------- *) @@ -466,6 +355,7 @@ let token s = >> (fun ((_,t),_) -> t);; let decimal = + let (||) = parser_or in let numeral = some isnum in let decimalint = atleast 1 numeral >> ((o) Num.num_of_string implode) in let decimalfrac = atleast 1 numeral @@ -485,13 +375,12 @@ let mkparser p s = let x,rst = p(explode s) in if rst = [] then x else failwith "mkparser: unparsed input";; -let parse_decimal = mkparser decimal;; - (* ------------------------------------------------------------------------- *) (* Parse back a vector. *) (* ------------------------------------------------------------------------- *) -let parse_sdpaoutput,parse_csdpoutput = +let _parse_sdpaoutput, parse_csdpoutput = + let (||) = parser_or in let vector = token "{" ++ listof decimal (token ",") "decimal" ++ token "}" >> (fun ((_,v),_) -> vector_of_list v) in @@ -508,23 +397,10 @@ let parse_sdpaoutput,parse_csdpoutput = mkparser sdpaoutput,mkparser csdpoutput;; (* ------------------------------------------------------------------------- *) -(* Also parse the SDPA output to test success (CSDP yields a return code). *) -(* ------------------------------------------------------------------------- *) - -let sdpa_run_succeeded = - let rec skipupto dscr prs inp = - (dscr ++ prs >> snd - || some (fun c -> true) ++ skipupto dscr prs >> snd) inp in - let prs = skipupto (word "phase.value" ++ token "=") - (possibly (a "p") ++ possibly (a "d") ++ - (word "OPT" || word "FEAS")) in - fun s -> try ignore (prs (explode s)); true with Noparse -> false;; - -(* ------------------------------------------------------------------------- *) (* The default parameters. Unfortunately this goes to a fixed file. *) (* ------------------------------------------------------------------------- *) -let sdpa_default_parameters = +let _sdpa_default_parameters = "100 unsigned int maxIteration;\ \n1.0E-7 double 0.0 < epsilonStar;\ \n1.0E2 double 0.0 < lambdaStar;\ @@ -555,7 +431,7 @@ let sdpa_alt_parameters = \n1.0E-7 double 0.0 < epsilonDash;\ \n";; -let sdpa_params = sdpa_alt_parameters;; +let _sdpa_params = sdpa_alt_parameters;; (* ------------------------------------------------------------------------- *) (* CSDP parameters; so far I'm sticking with the defaults. *) @@ -588,10 +464,10 @@ let run_csdp dbg obj mats = let input_file = Filename.temp_file "sos" ".dat-s" in let output_file = String.sub input_file 0 (String.length input_file - 6) ^ ".out" - and params_file = Filename.concat (!temp_path) "param.csdp" in + and params_file = Filename.concat temp_path "param.csdp" in file_of_string input_file (sdpa_of_problem "" obj mats); file_of_string params_file csdp_params; - let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^ + let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^ " " ^ output_file ^ (if dbg then "" else "> /dev/null")) in let op = string_of_file output_file in @@ -600,16 +476,6 @@ let run_csdp dbg obj mats = else (Sys.remove input_file; Sys.remove output_file)); rv,res);; -let csdp obj mats = - let rv,res = run_csdp (!debugging) obj mats in - (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible" - else if rv = 3 then () - (* Format.print_string "csdp warning: Reduced accuracy"; - Format.print_newline() *) - else if rv <> 0 then failwith("csdp: error "^string_of_int rv) - else ()); - res;; - (* ------------------------------------------------------------------------- *) (* Try some apparently sensible scaling first. Note that this is purely to *) (* get a cleaner translation to floating-point, and doesn't affect any of *) @@ -653,21 +519,7 @@ let linear_program_basic a = let mats = List.map (fun j -> diagonal (column j a)) (1--n) and obj = vector_const (Int 1) m in let rv,res = run_csdp false obj mats in - if rv = 1 or rv = 2 then false - else if rv = 0 then true - else failwith "linear_program: An error occurred in the SDP solver";; - -(* ------------------------------------------------------------------------- *) -(* Alternative interface testing A x >= b for matrix A, vector b. *) -(* ------------------------------------------------------------------------- *) - -let linear_program a b = - let m,n = dimensions a in - if dim b <> m then failwith "linear_program: incompatible dimensions" else - let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n) - and obj = vector_const (Int 1) m in - let rv,res = run_csdp false obj mats in - if rv = 1 or rv = 2 then false + if rv = 1 || rv = 2 then false else if rv = 0 then true else failwith "linear_program: An error occurred in the SDP solver";; @@ -716,40 +568,6 @@ let equation_eval assig eq = foldl (fun a v c -> a +/ value(v) */ c) (Int 0) eq;; (* ------------------------------------------------------------------------- *) -(* Eliminate among linear equations: return unconstrained variables and *) -(* assignments for the others in terms of them. We give one pseudo-variable *) -(* "one" that's used for a constant term. *) -(* ------------------------------------------------------------------------- *) - -let failstore = ref [];; - -let eliminate_equations = - let rec extract_first p l = - match l with - [] -> failwith "extract_first" - | h::t -> if p(h) then h,t else - let k,s = extract_first p t in - k,h::s in - let rec eliminate vars dun eqs = - match vars with - [] -> if forall is_undefined eqs then dun - else (failstore := [vars,dun,eqs]; raise Unsolvable) - | v::vs -> - try let eq,oeqs = extract_first (fun e -> defined e v) eqs in - let a = apply eq v in - let eq' = equation_cmul (Int(-1) // a) (undefine v eq) in - let elim e = - let b = tryapplyd e v (Int 0) in - if b =/ Int 0 then e else - equation_add e (equation_cmul (minus_num b // a) eq) in - eliminate vs ((v |-> eq') (mapf elim dun)) (List.map elim oeqs) - with Failure _ -> eliminate vs dun eqs in - fun one vars eqs -> - let assig = eliminate vars undefined eqs in - let vs = foldl (fun a x f -> subtract (dom f) [one] @ a) [] assig in - setify vs,assig;; - -(* ------------------------------------------------------------------------- *) (* Eliminate all variables, in an essentially arbitrary order. *) (* ------------------------------------------------------------------------- *) @@ -780,18 +598,6 @@ let eliminate_all_equations one = setify vs,assig;; (* ------------------------------------------------------------------------- *) -(* Solve equations by assigning arbitrary numbers. *) -(* ------------------------------------------------------------------------- *) - -let solve_equations one eqs = - let vars,assigs = eliminate_all_equations one eqs in - let vfn = itlist (fun v -> (v |-> Int 0)) vars (one |=> Int(-1)) in - let ass = - combine (+/) (fun c -> false) (mapf (equation_eval vfn) assigs) vfn in - if forall (fun e -> equation_eval ass e =/ Int 0) eqs - then undefine one ass else raise Sanity;; - -(* ------------------------------------------------------------------------- *) (* Hence produce the "relevant" monomials: those whose squares lie in the *) (* Newton polytope of the monomials in the input. (This is enough according *) (* to Reznik: "Extremal PSD forms with few terms", Duke Math. Journal, *) @@ -898,19 +704,6 @@ let epoly_pmul p q acc = a q) acc p;; (* ------------------------------------------------------------------------- *) -(* Usual operations on equation-parametrized poly. *) -(* ------------------------------------------------------------------------- *) - -let epoly_cmul c l = - if c =/ Int 0 then undefined else mapf (equation_cmul c) l;; - -let epoly_neg = epoly_cmul (Int(-1));; - -let epoly_add = combine equation_add is_undefined;; - -let epoly_sub p q = epoly_add p (epoly_neg q);; - -(* ------------------------------------------------------------------------- *) (* Convert regular polynomial. Note that we treat (0,0,0) as -1. *) (* ------------------------------------------------------------------------- *) @@ -953,11 +746,11 @@ let run_csdp dbg nblocks blocksizes obj mats = let input_file = Filename.temp_file "sos" ".dat-s" in let output_file = String.sub input_file 0 (String.length input_file - 6) ^ ".out" - and params_file = Filename.concat (!temp_path) "param.csdp" in + and params_file = Filename.concat temp_path "param.csdp" in file_of_string input_file (sdpa_of_blockproblem "" nblocks blocksizes obj mats); file_of_string params_file csdp_params; - let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^ + let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^ " " ^ output_file ^ (if dbg then "" else "> /dev/null")) in let op = string_of_file output_file in @@ -968,7 +761,7 @@ let run_csdp dbg nblocks blocksizes obj mats = let csdp nblocks blocksizes obj mats = let rv,res = run_csdp (!debugging) nblocks blocksizes obj mats in - (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible" + (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible" else if rv = 3 then () (*Format.print_string "csdp warning: Reduced accuracy"; Format.print_newline() *) @@ -988,8 +781,6 @@ let bmatrix_cmul c bm = let bmatrix_neg = bmatrix_cmul (Int(-1));; -let bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);; - (* ------------------------------------------------------------------------- *) (* Smash a block matrix into components. *) (* ------------------------------------------------------------------------- *) @@ -1102,15 +893,6 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = cfs,List.map (fun (a,b) -> snd a,b) msq;; (* ------------------------------------------------------------------------- *) -(* Iterative deepening. *) -(* ------------------------------------------------------------------------- *) - -let rec deepen f n = - try print_string "Searching with depth limit "; - print_int n; print_newline(); f n - with Failure _ -> deepen f (n + 1);; - -(* ------------------------------------------------------------------------- *) (* The ordering so we can create canonical HOL polynomials. *) (* ------------------------------------------------------------------------- *) @@ -1136,10 +918,6 @@ let monomial_order = if deg1 < deg2 then false else if deg1 > deg2 then true else lexorder mon1 mon2;; -let dest_poly p = - List.map (fun (m,c) -> c,dest_monomial m) - (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p));; - (* ------------------------------------------------------------------------- *) (* Map back polynomials and their composites to HOL. *) (* ------------------------------------------------------------------------- *) @@ -1373,9 +1151,6 @@ let rec allpermutations l = itlist (fun h acc -> List.map (fun t -> h::t) (allpermutations (subtract l [h])) @ acc) l [];; -let allvarorders l = - List.map (fun vlis x -> index x vlis) (allpermutations l);; - let changevariables_monomial zoln (m:monomial) = foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;; @@ -1392,15 +1167,6 @@ let sdpa_of_vector (v:vector) = let strs = List.map (o (decimalize 20) (element v)) (1--n) in end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";; -let sdpa_of_blockdiagonal k m = - let pfx = string_of_int k ^" " in - let ents = - foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in - let entss = sort (increasing fst) ents in - itlist (fun ((b,i,j),c) a -> - pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ - " " ^ decimalize 20 c ^ "\n" ^ a) entss "";; - let sdpa_of_matrix k (m:matrix) = let pfx = string_of_int k ^ " 1 " in let ms = foldr (fun (i,j) c a -> if i > j then a else ((i,j),c)::a) @@ -1425,10 +1191,10 @@ let run_csdp dbg obj mats = let input_file = Filename.temp_file "sos" ".dat-s" in let output_file = String.sub input_file 0 (String.length input_file - 6) ^ ".out" - and params_file = Filename.concat (!temp_path) "param.csdp" in + and params_file = Filename.concat temp_path "param.csdp" in file_of_string input_file (sdpa_of_problem "" obj mats); file_of_string params_file csdp_params; - let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^ + let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^ " " ^ output_file ^ (if dbg then "" else "> /dev/null")) in let op = string_of_file output_file in @@ -1439,7 +1205,7 @@ let run_csdp dbg obj mats = let csdp obj mats = let rv,res = run_csdp (!debugging) obj mats in - (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible" + (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible" else if rv = 3 then () (* (Format.print_string "csdp warning: Reduced accuracy"; Format.print_newline()) *) diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index f54914f25..6b8b820ac 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -525,7 +525,7 @@ let isspace,issep,isbra,issymb,isalpha,isnum,isalnum = and isalnum c = Array.get ctable (charcode c) >= 16 in isspace,issep,isbra,issymb,isalpha,isnum,isalnum;; -let (||) parser1 parser2 input = +let parser_or parser1 parser2 input = try parser1 input with Noparse -> parser2 input;; @@ -571,7 +571,7 @@ let finished input = (* ------------------------------------------------------------------------- *) -let temp_path = ref Filename.temp_dir_name;; +let temp_path = Filename.get_temp_dir_name ();; (* ------------------------------------------------------------------------- *) (* Convenient conversion between files and (lists of) strings. *) diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index b1ff59e78..a120d4efb 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)^"]" (*********************************************************************** @@ -197,8 +196,6 @@ module Hashpol = Hashtbl.Make( (* A pretty printer for polynomials, with Maple-like syntax. *) -open Format - let getvar lv i = try (List.nth lv i) with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv) @@ -252,59 +249,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 +539,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 db8f3e4b2..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 *) @@ -437,7 +409,7 @@ open Ideal that has the same size than lp and where true indicates an element that has been removed *) -let rec clean_pol lp = +let clean_pol lp = let t = Hashpol.create 12 in let find p = try Hashpol.find t p with 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/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index dd68eac24..d59ffee54 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -19,7 +19,6 @@ open Environ open Libnames open Globnames open Glob_term -open Tacticals open Tacexpr open Coqlib open Mod_subst @@ -279,8 +278,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/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 4367d021c..d9d32c681 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -7,13 +7,10 @@ (************************************************************************) open Names -open Constr open EConstr open Libnames open Globnames open Constrexpr -open Tacexpr -open Proof_type open Newring_ast val protect_tac_in : string -> Id.t -> unit Proofview.tactic diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index f3555ebc4..72c70750c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -21,30 +21,21 @@ open Pp open Pcoq open Genarg open Stdarg -open Tacarg open Term open Vars -open Topconstr open Libnames open Tactics open Tacticals open Termops -open Namegen open Recordops open Tacmach -open Coqlib open Glob_term open Util open Evd -open Extend -open Goptions open Tacexpr -open Proofview.Notations open Tacinterp open Pretyping open Constr -open Pltac -open Extraargs open Ppconstr open Printer @@ -54,14 +45,9 @@ open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops -open Notation_term -open Notation_ops -open Locus -open Locusops DECLARE PLUGIN "ssrmatching_plugin" -type loc = Loc.t let dummy_loc = Loc.ghost let errorstrm = CErrors.user_err ~hdr:"ssrmatching" let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) @@ -90,8 +76,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 +288,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 +353,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,16 +417,10 @@ 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 -exception UndefPat - let hole_var = mkVar (id_of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = @@ -917,13 +888,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 +1009,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 @@ -1261,7 +1224,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in - let concl = find_T env0 concl0 1 do_subst in + let concl = find_T env0 concl0 1 ~k:do_subst in let _ = end_T () in concl | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> @@ -1273,11 +1236,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = (* we start from sigma, so hole is considered a rigid head *) let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in - let concl = find_T env0 concl0 1 (fun env c _ h -> + let concl = find_T env0 concl0 1 ~k:(fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h - (fun env _ -> do_subst env e_body))) in + ~k:(fun env _ -> do_subst env e_body))) in let _ = end_X () in let _ = end_T () in concl | Some (sigma, E_In_X_In_T (e, hole, p)) -> @@ -1289,11 +1252,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_X, end_X = mk_tpattern_matcher sigma noindex holep in let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in - let concl = find_T env0 concl0 1 (fun env c _ h -> + let concl = find_T env0 concl0 1 ~k:(fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> - find_E env e_body h do_subst))) in + fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> + find_E env e_body h ~k:do_subst))) in let _ = end_E () in let _ = end_X () in let _ = end_T () in concl | Some (sigma, E_As_X_In_T (e, hole, p)) -> @@ -1306,10 +1269,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher sigma occ holep in - let concl = find_TE env0 concl0 1 (fun env c _ h -> + let concl = find_TE env0 concl0 1 ~k:(fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> + fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in let e_body = fs e_sigma e in do_subst env e_body e_body h))) in @@ -1352,7 +1315,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let ise, u = mk_tpattern env sigma0 (ise,EConstr.Unsafe.to_constr t) ok L2R p in let find_U, end_U = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - let concl = find_U env concl h (fun _ _ _ -> mkRel) in + let concl = find_U env concl h ~k:(fun _ _ _ -> mkRel) in let rdx, _, (sigma, uc, p) = end_U () in sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 894cdb943..638b4e254 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -4,7 +4,6 @@ open Genarg open Tacexpr open Environ -open Tacmach open Evd open Proof_type open Term @@ -226,7 +225,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/cbv.mli b/pretyping/cbv.mli index b014af2c7..eb25994be 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 e9b3d197b..32da81f96 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 0d741a5a5..c4238e8b0 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 542db7fdf..c26e7458e 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 bc63d092d..ea3d3f0fa 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 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/pretyping/detyping.ml b/pretyping/detyping.ml index 8ba408679..483e2b432 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 4bb66b8e9..305eae15a 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 fc07f0fbe..7cee1e8a7 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 c5ae684e3..5fd104c78 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 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/find_subterm.mli b/pretyping/find_subterm.mli index e3d3b74f1..d22f94e4e 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 5b42add28..429e5005e 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 b16d04495..33a68589c 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 5694d345c..791fd74ed 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 24f6d1689..f9cf6b83b 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 ae87cd8c0..68ef97659 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 caa5a5c8a..42acc5705 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 270320538..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 @@ -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 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/tacred.mli b/pretyping/tacred.mli index 76d0bc241..c31212e26 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 2db0e9e88..754dacd19 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 9bd430e4d..558575ccc 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 532cc8baa..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 @@ -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 f0c8cd58c..3e41439c8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -394,10 +394,6 @@ open Decl_kinds (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ 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/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/printing/prettyp.mli b/printing/prettyp.mli index 38e111034..6841781cc 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -8,7 +8,6 @@ open Pp open Names -open Term open Environ open Reductionops open Libnames 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/clenvtac.mli b/proofs/clenvtac.mli index 5b7164705..26069207e 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,6 @@ (** Legacy components of the previous proof engine. *) -open Term open Clenv open EConstr open Unification diff --git a/proofs/goal.ml b/proofs/goal.ml index 9046f4534..fc8e635a0 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -8,7 +8,6 @@ open Util open Pp -open Term open Sigma.Notations module NamedDecl = Context.Named.Declaration 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/proof_type.mli b/proofs/proof_type.mli index 03bc5e471..e59db9e42 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -11,9 +11,6 @@ open Evd open Names open Term -open Glob_term -open Nametab -open Misctypes (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 0fe5c73f1..cb3538422 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -43,7 +43,7 @@ let cbv_native env sigma c = let whd_cbn flags env sigma t = let (state,_) = - (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) + (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty)) in Reductionops.Stack.zip ~refold:true sigma state diff --git a/proofs/refiner.ml b/proofs/refiner.ml index bc12b3ba7..259e96a27 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Evd -open Environ open Proof_type open Logic 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/proofs/tacmach.mli b/proofs/tacmach.mli index 627a8e0e7..e6e60e27f 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -15,7 +15,6 @@ open Proof_type open Redexpr open Pattern open Locus -open Misctypes (** Operations for handling terms under a local typing context. *) diff --git a/stm/stm.ml b/stm/stm.ml index e823373f7..84c8aa9a9 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 @@ -1212,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 @@ -1281,7 +1276,6 @@ end = struct (* {{{ *) | RespBuiltProof of Proof_global.closed_proof_output * float | RespError of error | RespStates of (Stateid.t * State.partial_state) list - | RespDone let name = ref "proofworker" let extra_env () = !async_proofs_workers_extra_env @@ -1380,7 +1374,7 @@ end = struct (* {{{ *) if not drop then begin let checked_proof = Future.chain ~pure:false future_proof (fun p -> let pobject, _ = - Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in + Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in stm_vernac_interp stop @@ -2326,6 +2320,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach ~redefine_qed id end (* }}} *) +[@@@ocaml.warning "+60"] (********************************* STM API ************************************) (******************************************************************************) @@ -2432,7 +2427,7 @@ let merge_proof_branch ~valid ?id qast keep brname = let id = VCS.new_node ?id () in VCS.merge id ~ours:(Qed (qed None)) brname; VCS.delete_branch brname; - VCS.propagate_sideff None; + VCS.propagate_sideff ~replay:None; `Ok | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = diff --git a/stm/stm.mli b/stm/stm.mli index 30e9629c6..d2bee4496 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -6,10 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Vernacexpr open Names -open Feedback -open Loc (** state-transaction-machine interface *) 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/tactics/auto.ml b/tactics/auto.ml index 42230dff1..c2d12ebd0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,16 +10,12 @@ module CVars = Vars open Pp open Util -open CErrors open Names -open Vars 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/auto.mli b/tactics/auto.mli index 32710e347..9ed9f0ae2 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -9,7 +9,6 @@ (** This files implements auto and related automation tactics *) open Names -open Term open EConstr open Clenv open Pattern diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 2a5e7c345..27f624f71 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Pattern open Names diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 54e4405d1..2d6dffdd2 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -18,9 +18,7 @@ open Names open Term open Termops open EConstr -open Reduction open Proof_type -open Tacticals open Tacmach open Tactics open Clenv @@ -357,12 +355,12 @@ let shelve_dependencies gls = let hintmap_of sigma hdc secvars concl = match hdc with - | None -> fun db -> Hint_db.map_none secvars db + | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> fun db -> if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto sigma secvars hdc concl db - else Hint_db.map_existential sigma secvars hdc concl db + Hint_db.map_eauto sigma ~secvars hdc concl db + else Hint_db.map_existential sigma ~secvars hdc concl db (** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db only_classes db_list local_db secvars = @@ -1219,7 +1217,6 @@ module Search = struct let intro_tac info kont gl = let open Proofview in - let open Proofview.Notations in let env = Goal.env gl in let sigma = Goal.sigma gl in let s = Sigma.to_evar_map sigma in @@ -1257,7 +1254,6 @@ module Search = struct let search_tac_gl ?st only_classes dep hints depth i sigma gls gl : unit Proofview.tactic = let open Proofview in - let open Proofview.Notations in if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") else diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 738cc0feb..c5731e377 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -9,9 +9,7 @@ (** This files implements typeclasses eauto *) open Names -open Constr open EConstr -open Tacmach val catchable : exn -> bool diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 510b135b0..2cf5a6829 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr open Misctypes diff --git a/tactics/eauto.mli b/tactics/eauto.mli index e2006ac1e..c952f4e72 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr -open Proof_type open Hints open Tactypes diff --git a/tactics/elim.ml b/tactics/elim.ml index e37ec6bce..855cb206f 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -8,7 +8,6 @@ open Util open Names -open Term open Termops open EConstr open Inductiveops diff --git a/tactics/elim.mli b/tactics/elim.mli index dc1af79ba..fb7cc7b83 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Tacticals open Misctypes diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index bac3980d2..5012b0ef7 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -25,7 +25,6 @@ open Constr_matching open Misctypes open Tactypes open Hipattern -open Pretyping open Proofview.Notations open Tacmach.New open Coqlib diff --git a/tactics/equality.ml b/tactics/equality.ml index 25c28cf4a..cc7701ad5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -14,7 +14,6 @@ open Names open Nameops open Term open Termops -open Environ open EConstr open Vars open Namegen diff --git a/tactics/equality.mli b/tactics/equality.mli index 5467b4af2..d979c580a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -8,7 +8,6 @@ (*i*) open Names -open Term open Evd open EConstr open Environ diff --git a/tactics/hints.ml b/tactics/hints.ml index bcc068d3d..240178c9a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1435,7 +1435,7 @@ let pr_hints_db (name,db,hintlist) = let pr_hint_list_for_head c = let dbs = current_db () in let validate (name, db) = - let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in + let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in (name, db, hints) in let valid_dbs = List.map validate dbs in diff --git a/tactics/hints.mli b/tactics/hints.mli index 467fd46d5..3a0339ff5 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -9,7 +9,6 @@ open Pp open Util open Names -open Term open EConstr open Environ open Globnames 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/hipattern.mli b/tactics/hipattern.mli index dd09c3a4d..82a3d47b5 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Evd open EConstr open Coqlib diff --git a/tactics/inv.ml b/tactics/inv.ml index 904a17417..266cac5c7 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Termops -open Environ open EConstr open Vars open Namegen diff --git a/tactics/inv.mli b/tactics/inv.mli index 446a62f6d..5835e763d 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Misctypes open Tactypes diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 26d4ac994..a343fc81a 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Constrexpr open Misctypes diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4173f8734..211a7338b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5040,10 +5040,6 @@ end (** Tacticals defined directly in term of Proofview *) module New = struct - open Proofview.Notations - - let exact_proof c = exact_proof c - open Genredexpr open Locus diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 2c863c42a..726fd23b6 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -49,7 +49,7 @@ struct | DNil (* debug *) - let pr_dconstr f : 'a t -> std_ppcmds = function + let _pr_dconstr f : 'a t -> std_ppcmds = function | DRel -> str "*" | DSort -> str "Sort" | DRef _ -> str "Ref" diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ed89bda2c..4875cb62b 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -56,48 +56,48 @@ let lib_dirs = let usage () = - output_string stderr "Usage summary: - -coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}] - ... [any] ... [-extra[-phony] result dependencies command] - ... [-I dir] ... [-R physicalpath logicalpath] - ... [-Q physicalpath logicalpath] ... [VARIABLE = value] - ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] - [-h] [--help] - -[file.v]: Coq file to be compiled -[file.ml[i4]?]: Objective Caml file to be compiled -[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml - library/module -[any] : subdirectory that should be \"made\" and has a Makefile itself - to do so. Very fragile and discouraged. -[-extra result dependencies command]: add target \"result\" with command - \"command\" and dependencies \"dependencies\". If \"result\" is not - generic (do not contains a %), \"result\" is built by _make all_ and - deleted by _make clean_. -[-extra-phony result dependencies command]: add a PHONY target \"result\" - with command \"command\" and dependencies \"dependencies\". Note that - _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as - as a dependencies of an already defined target \"foo\". -[-I dir]: look for Objective Caml dependencies in \"dir\" -[-R physicalpath logicalpath]: look for Coq dependencies resursively - starting from \"physicalpath\". The logical path associated to the - physical path is \"logicalpath\". -[-Q physicalpath logicalpath]: look for Coq dependencies starting from - \"physicalpath\". The logical path associated to the physical path - is \"logicalpath\". -[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" -[-byte]: compile with byte-code version of coq -[-opt]: compile with native-code version of coq -[-arg opt]: send option \"opt\" to coqc -[-install opt]: where opt is \"user\" to force install into user directory, - \"none\" to build a makefile with no install target or - \"global\" to force install in $COQLIB directory -[-f file]: take the contents of file as arguments -[-o file]: output should go in file file - Output file outside the current directory is forbidden. -[-h]: print this usage summary -[--help]: equivalent to [-h]\n"; + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n\ +\n[file.v]: Coq file to be compiled\ +\n[file.ml[i4]?]: Objective Caml file to be compiled\ +\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ +\n library/module\ +\n[any] : subdirectory that should be \"made\" and has a Makefile itself\ +\n to do so. Very fragile and discouraged.\ +\n[-extra result dependencies command]: add target \"result\" with command\ +\n \"command\" and dependencies \"dependencies\". If \"result\" is not\ +\n generic (do not contains a %), \"result\" is built by _make all_ and\ +\n deleted by _make clean_.\ +\n[-extra-phony result dependencies command]: add a PHONY target \"result\"\ +\n with command \"command\" and dependencies \"dependencies\". Note that\ +\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ +\n as a dependencies of an already defined target \"foo\".\ +\n[-I dir]: look for Objective Caml dependencies in \"dir\"\ +\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ +\n starting from \"physicalpath\". The logical path associated to the\ +\n physical path is \"logicalpath\".\ +\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ +\n \"physicalpath\". The logical path associated to the physical path\ +\n is \"logicalpath\".\ +\n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\ +\n[-byte]: compile with byte-code version of coq\ +\n[-opt]: compile with native-code version of coq\ +\n[-arg opt]: send option \"opt\" to coqc\ +\n[-install opt]: where opt is \"user\" to force install into user directory,\ +\n \"none\" to build a makefile with no install target or\ +\n \"global\" to force install in $COQLIB directory\ +\n[-f file]: take the contents of file as arguments\ +\n[-o file]: output should go in file file\ +\n Output file outside the current directory is forbidden.\ +\n[-h]: print this usage summary\ +\n[--help]: equivalent to [-h]\n"; exit 1 let is_genrule r = (* generic rule (like bar%foo: ...) *) @@ -264,8 +264,8 @@ let where_put_doc = function then physical_dir_of_logical_dir pr else - let () = prerr_string "Warning: -Q options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n" in + let () = prerr_string ("Warning: -Q options don't have a correct common prefix," + ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in "$(INSTALLDEFAULTROOT)" |_,inc_i,((_,lp,_)::q as inc_r) -> let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in @@ -277,8 +277,8 @@ let where_put_doc = function then physical_dir_of_logical_dir pr else - let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n" in + let () = prerr_string ("Warning: -R/-Q options don't have a correct common prefix," + ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in "$(INSTALLDEFAULTROOT)" let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function @@ -518,8 +518,8 @@ let variables is_install opt (args,defs) = if !some_ml4file || !some_mlfile || !some_mlifile then begin print "COQSRCLIBS?=" ; List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ; - List.iter (fun c -> print " \\ - -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; + List.iter (fun c -> print " \\\ +\n -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n"; print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n"; @@ -529,8 +529,8 @@ let variables is_install opt (args,defs) = print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n"; - print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ - $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\\ +\n $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with | Project_file.NoInstall -> () @@ -816,14 +816,14 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = let banner () = print (Printf.sprintf -"############################################################################# -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \\VV/ # ## -## // # Makefile automagically generated by coq_makefile V%s ## -############################################################################# - -" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' ')) +"#############################################################################\ +\n## v # The Coq Proof Assistant ##\ +\n## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##\ +\n## \\VV/ # ##\ +\n## // # Makefile automagically generated by coq_makefile V%s ##\ +\n#############################################################################\ +\n\n" +(Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' ')) let warning () = print "# WARNING\n#\n"; diff --git a/tools/coqc.ml b/tools/coqc.ml index b12d48710..552a943c8 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -77,12 +77,12 @@ let parse_args () = | ("-v"|"--version") :: _ -> Usage.version 0 | ("-where") :: _ -> - Envars.set_coqlib (fun x -> x); + Envars.set_coqlib ~fail:(fun x -> x); print_endline (Envars.coqlib ()); exit 0 | ("-config" | "--config") :: _ -> - Envars.set_coqlib (fun x -> x); + Envars.set_coqlib ~fail:(fun x -> x); Usage.print_config (); exit 0 diff --git a/tools/coqdep.ml b/tools/coqdep.ml index a9f1b7376..1c1c1be6a 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -502,7 +502,7 @@ let coqdep () = let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) - (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x))); + (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x))); List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; 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/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. *) diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 66bbf43f6..13e860a88 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp - (** The Coq toplevel loop. *) (** A buffer for the character read from a channel. We store the command diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9cf075065..c3a755860 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -292,7 +292,7 @@ let init_gc () = between coqtop and coqc. *) let usage () = - Envars.set_coqlib CErrors.error; + Envars.set_coqlib ~fail:CErrors.error; init_load_path (); if !batch_mode then Usage.print_usage_coqc () else begin @@ -609,7 +609,7 @@ let init_toplevel arglist = (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); - Envars.set_coqlib CErrors.error; + Envars.set_coqlib ~fail:CErrors.error; if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); if !print_config then (Usage.print_config (); exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 66f782ffb..e457ca61d 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -83,7 +83,7 @@ let print_usage_channel co command = \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -\n for full Gc stats dump) +\n for full Gc stats dump)\ \n -native-compiler precompile files for the native_compute machinery\ \n -h, -help, --help print this list of options\ \n"; diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9ff320ee8..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 = @@ -125,7 +124,7 @@ let rec interp_vernac sid (loc,com) = let f = Loadpath.locate_file fname in load_vernac verbosely sid f | v -> - let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in + let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in (* Main STM interaction *) if ntip <> `NewTip then diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index c91dcc505..f363deac6 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -9,7 +9,6 @@ (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) -open Tacmach open CErrors open Util open Pp @@ -28,8 +27,6 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration -let out_punivs = Univ.out_punivs - (**********************************************************************) (* Generic synthesis of boolean equality *) @@ -718,7 +715,6 @@ let compute_lb_goal ind lnamesparrec nparrec = ))), eff let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = - let open EConstr in let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = diff --git a/vernac/class.ml b/vernac/class.ml index 95114ec39..104f3c1db 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -311,7 +311,7 @@ let add_coercion_hook poly local ref = | Global -> false | Discharge -> assert false in - let () = try_add_new_coercion ref stre poly in + let () = try_add_new_coercion ref ~local:stre poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg @@ -324,6 +324,6 @@ let add_subclass_hook poly local ref = | Discharge -> assert false in let cl = class_of_global ref in - try_add_new_coercion_subclass cl stre poly + try_add_new_coercion_subclass cl ~local:stre poly let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly) diff --git a/vernac/classes.ml b/vernac/classes.ml index 833719965..d515b0c9b 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -66,8 +66,6 @@ let _ = Hook.set Typeclasses.classes_transparent_state_hook (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) -open Vernacexpr - (** TODO: add subinstances *) let existing_instance glob g info = let c = global g in diff --git a/vernac/command.ml b/vernac/command.ml index 3ea8f6590..2fa2aa4e3 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -258,7 +258,7 @@ match local with let () = Universes.register_universe_binders gr pl in let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in - let () = if is_coe then Class.try_add_new_coercion gr local p in + let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = if p (* polymorphic *) then Univ.UContext.instance ctx else Univ.Instance.empty @@ -752,7 +752,7 @@ let do_mutual_inductive indl poly prv finite = (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml index 85d0b6194..c6588684a 100644 --- a/vernac/ind_tables.ml +++ b/vernac/ind_tables.ml @@ -151,7 +151,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Safe_typing.add_private - (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff + (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -172,7 +172,7 @@ let define_mutual_scheme_base kind suff f mode names mind = consts, Safe_typing.add_private (Safe_typing.private_con_of_scheme - kind (Global.safe_env()) (Array.to_list schemes)) + ~kind (Global.safe_env()) (Array.to_list schemes)) eff let define_mutual_scheme kind mode names mind = @@ -185,7 +185,7 @@ let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in s, Safe_typing.add_private (Safe_typing.private_con_of_scheme - kind (Global.safe_env()) [ind, s]) + ~kind (Global.safe_env()) [ind, s]) Safe_typing.empty_private_constants let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f805eeaa9..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 @@ -1196,7 +1196,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze `No in + let fs = Lib.freeze ~marshallable:`No in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 11366fe91..a276f9f9a 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,7 +12,6 @@ open Evd open Names open Pp open Globnames -open Vernacexpr open Decl_kinds (** Forward declaration. *) 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/search.ml b/vernac/search.ml index 6279b17ae..5b6e9a9c3 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -14,11 +14,9 @@ open Declarations open Libobject open Environ open Pattern -open Printer open Libnames open Globnames open Nametab -open Goptions module NamedDecl = Context.Named.Declaration diff --git a/vernac/search.mli b/vernac/search.mli index 82b79f75d..e34522d8a 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Environ diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index a1835959c..6d9d71a62 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 () @@ -133,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)) @@ -283,16 +280,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 *) |