diff options
77 files changed, 10 insertions, 292 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 2bd67dcdc..c5dfe3033 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -8,7 +8,6 @@ open Errors open Util -open Pp open Names open Term open Vars diff --git a/engine/evd.ml b/engine/evd.ml index b6849f7ff..b883db615 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -363,7 +363,6 @@ open Misctypes type t val empty : t -val add_name_newly_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t val remove_name_defined : Evar.t -> t -> t val rename : Evar.t -> Id.t -> t -> t diff --git a/engine/geninterp.ml b/engine/geninterp.ml index 45b0aa231..cfca95d3e 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -32,7 +32,7 @@ struct let repr = ValT.repr let create = ValT.create - let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t) + let pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t) let typ_list = ValT.create "list" let typ_opt = ValT.create "option" diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 4b78bc05d..d67f1eee3 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -340,7 +340,6 @@ struct let lift = BackState.lift let once = BackState.once let break = BackState.break - let reflect = BackState.reflect let split = BackState.split let repr = BackState.repr diff --git a/engine/proofview.ml b/engine/proofview.ml index ba664cafa..95e20bc25 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -925,8 +925,6 @@ end module UnsafeRepr = Proof.Unsafe let (>>=) = tclBIND -let (<*>) = tclTHEN -let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) (** {6 Goal-dependent tactics} *) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index aa1a75db6..6639b0201 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -44,12 +44,9 @@ module SentenceId : sig val mk_sentence : start:GText.mark -> stop:GText.mark -> flag list -> sentence - val set_flags : sentence -> flag list -> unit val add_flag : sentence -> flag -> unit val has_flag : sentence -> mem_flag -> bool val remove_flag : sentence -> mem_flag -> unit - val same_sentence : sentence -> sentence -> bool - val hidden_edit_id : unit -> int val find_all_tooltips : sentence -> int -> string list val add_tooltip : sentence -> int -> int -> string -> unit val set_index : sentence -> int -> unit @@ -87,18 +84,15 @@ end = struct index = -1; changed_sig = new GUtil.signal (); } - let hidden_edit_id () = decr id; !id let changed s = s.changed_sig#call (s.index, List.map mem_flag_of_flag s.flags) - let set_flags s f = s.flags <- f; changed s let add_flag s f = s.flags <- CList.add_set (=) f s.flags; changed s let has_flag s mf = List.exists (fun f -> mem_flag_of_flag f = mf) s.flags let remove_flag s mf = s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags; changed s - let same_sentence s1 s2 = s1.edit_id = s2.edit_id let find_all_tooltips s off = CList.map_filter (fun (start,stop,t) -> if start <= off && off <= stop then Some t else None) diff --git a/ide/preferences.ml b/ide/preferences.ml index addea9074..c4dc55972 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -386,14 +386,6 @@ let processing_color = let _ = attach_bg processing_color Tags.Script.to_process let _ = attach_bg processing_color Tags.Script.incomplete -let default_tag = { - tag_fg_color = None; - tag_bg_color = None; - tag_bold = false; - tag_italic = false; - tag_underline = false; -} - let tags = ref Util.String.Map.empty let list_tags () = !tags diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml index 580f1fbcb..8f6cb382a 100644 --- a/ide/utils/okey.ml +++ b/ide/utils/okey.ml @@ -52,33 +52,6 @@ let int_of_modifier = function | `RELEASE -> 1 lsl 30 | `SUPER -> 1 lsl 21 -let print_modifier l = - List.iter - (fun m -> - print_string - (((function - `SHIFT -> "SHIFT" - | `LOCK -> "LOCK" - | `CONTROL -> "CONTROL" - | `MOD1 -> "MOD1" - | `MOD2 -> "MOD2" - | `MOD3 -> "MOD3" - | `MOD4 -> "MOD4" - | `MOD5 -> "MOD5" - | `BUTTON1 -> "B1" - | `BUTTON2 -> "B2" - | `BUTTON3 -> "B3" - | `BUTTON4 -> "B4" - | `BUTTON5 -> "B5" - | `HYPER -> "HYPER" - | `META -> "META" - | `RELEASE -> "" - | `SUPER -> "SUPER") - m)^" ") - ) - l; - print_newline () - let int_of_modifiers l = List.fold_left (fun acc -> fun m -> acc + (int_of_modifier m)) 0 l diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 6c53fc013..aeae3e1fd 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -86,7 +86,7 @@ let signals = [ end_s#disconnect; ] in object (self : 'a) - inherit GUtil.ml_signals signals as super + inherit GUtil.ml_signals signals method start_completion = start_s#connect ~after method update_completion = update_s#connect ~after method end_completion = end_s#connect ~after diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 4d95fdd0d..47c86045a 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -91,7 +91,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let () = proof#buffer#insert head_str in let () = insert_hyp hyps_hints hyps in let () = - let tags = Tags.Proof.goal :: if goal_hints <> [] then + let _ = if goal_hints <> [] then let tag = proof#buffer#create_tag [] in let () = hook_tag_cb tag goal_hints sel_cb on_hover in [tag] diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 83fbda487..218cedb36 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -287,7 +287,7 @@ let completion = new Wg_Completion.complete_model ct view#buffer in let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in object (self) - inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super + inherit GSourceView2.source_view (Gobject.unsafe_cast tv) val undo_manager = new undo_manager view#buffer diff --git a/interp/constrarg.ml b/interp/constrarg.ml index b8f97e77c..011b31d9a 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -8,7 +8,6 @@ open Loc open Tacexpr -open Term open Misctypes open Genarg open Geninterp @@ -49,9 +48,6 @@ let wit_quant_hyp = make0 "quant_hyp" let wit_constr = make0 "constr" -let wit_constr_may_eval = - make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval" - let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" @@ -60,9 +56,6 @@ let wit_constr_with_bindings = make0 "constr_with_bindings" let wit_bindings = make0 "bindings" -let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = - make0 "hyp_location_flag" - let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = diff --git a/interp/notation.ml b/interp/notation.ml index b8f4f3201..0a65dfc09 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -13,7 +13,6 @@ open Pp open Bigint open Names open Term -open Nametab open Libnames open Globnames open Constrexpr diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index f9cf2691e..a705e3004 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -184,9 +184,6 @@ let rec pp_struct_const = function let pp_lbl lbl = str "L" ++ int lbl -let pp_pcon (id,u) = - pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" - let pp_fv_elem = function | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")" | FVrel i -> str "Rel(" ++ int i ++ str ")" diff --git a/kernel/names.ml b/kernel/names.ml index 8e0237863..e8226d3d3 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -341,7 +341,7 @@ module ModPath = struct | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l) - let rec eq d1 d2 = + let eq d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 7ac5b8d7b..4ed926f1f 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors open Names -open Univ open Nativelib open Reduction open Util diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 0e56e76aa..c30789641 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,7 +15,6 @@ open Util open Names -open Univ open Term open Declarations open Context.Named.Declaration diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f23ed16f0..5bf369441 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -20,7 +20,6 @@ open Util open Names open Term open Vars -open Univ open Environ open Closure open Esubst diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 4610dbcb0..89e833254 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -1,13 +1,9 @@ open Util open Names -open Term open Environ -open Conv_oracle open Reduction -open Closure open Vm open Csymtable -open Univ let val_of_constr env c = val_of_constr (pre_env env) c diff --git a/lib/spawn.ml b/lib/spawn.ml index fda4b4239..2b9c4ccac 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -78,20 +78,6 @@ let accept (sr,sw) = set_binary_mode_out cout true; (csr, csw), cin, cout -let handshake cin cout = - try - output_value cout (Hello (proto_version,Unix.getpid ())); flush cout; - match input_value cin with - | Hello(v, pid) when v = proto_version -> - prerr_endline (Printf.sprintf "Handshake with %d OK" pid); - pid - | _ -> raise (Failure "handshake protocol") - with - | Failure s | Invalid_argument s | Sys_error s -> - pr_err ("Handshake failed: " ^ s); raise (Failure "handshake") - | End_of_file -> - pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") - let spawn_sock env prog args = let main_sock, main_sock_name = mk_socket_channel () in let extra = [| prog; "-main-channel"; main_sock_name |] in diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 6c02a7202..8b5f527cd 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -13,14 +13,9 @@ open Names open Locus open Misctypes open Genredexpr -open Stdarg open Constrarg open Extraargs -open Pcoq.Constr -open Pcoq.Prim -open Pcoq.Tactic -open Proofview.Notations open Sigma.Notations DECLARE PLUGIN "coretactics" diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 79f80260f..1f3eb1335 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -14,13 +14,11 @@ open Stdarg open Constrarg open Extraargs open Pcoq.Prim -open Pcoq.Constr open Pcoq.Tactic open Mod_subst open Names open Tacexpr open Glob_ops -open Tactics open Errors open Util open Evd @@ -128,7 +126,6 @@ TACTIC EXTEND ediscriminate [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ] END -open Proofview.Notations let discrHyp id = Proofview.tclEVARMAP >>= fun sigma -> discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } @@ -458,8 +455,6 @@ TACTIC EXTEND evar | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END -open Tacticals - TACTIC EXTEND instantiate [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ] diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index 9ef154541..77075ec4c 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -10,8 +10,6 @@ open Misctypes open Class_tactics -open Pcoq.Prim -open Pcoq.Constr open Pcoq.Tactic open Stdarg open Constrarg diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index df499a2c9..1bbdb1779 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -307,7 +307,6 @@ GEXTEND Gram ; END -open Stdarg open Constrarg open Vernacexpr open Vernac_classifier diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index f2dbb5b6c..39db6268b 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -7,11 +7,9 @@ (************************************************************************) open Util -open Genarg open Pp open Names open Tacexpr -open Geninterp (** Tactic notations (TacAlias) *) diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 977c56f38..3744449e9 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -475,9 +475,6 @@ let clause_app f = function | { onhyps=Some l; concl_occs=nl } -> { onhyps=Some(List.map f l); concl_occs=nl} -let map_raw wit f ist x = - in_gen (glbwit wit) (f ist (out_gen (rawwit wit) x)) - (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *) let rec intern_atomic lf ist x = match (x:raw_atomic_tactic_expr) with diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 31bccd019..6a5d1380d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -21,7 +21,6 @@ open Libnames open Globnames open Nametab open Pfedit -open Proof_type open Refiner open Tacmach.New open Tactic_debug @@ -35,8 +34,6 @@ open Stdarg open Constrarg open Printer open Pretyping -module Monad_ = Monad -open Evd open Misctypes open Locus open Tacintern @@ -196,7 +193,7 @@ module Value = struct | OptArg t -> Val.Opt (tag_of_arg t) | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) - let rec val_cast arg v = prj (tag_of_arg arg) v + let val_cast arg v = prj (tag_of_arg arg) v let cast (Topwit wit) v = val_cast wit v @@ -695,13 +692,6 @@ let pf_interp_casted_constr ist gl c = let pf_interp_constr ist gl = interp_constr ist (pf_env gl) (project gl) -let new_interp_constr ist c k = - let open Proofview in - Proofview.Goal.s_enter { s_enter = begin fun gl -> - let (sigma, c) = interp_constr ist (Goal.env gl) (project gl) c in - Sigma.Unsafe.of_pair (k c, sigma) - end } - let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with @@ -1290,7 +1280,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run tac (fun () -> Proofview.tclUNIT ()) | TacML (loc,opn,l) -> - let open Ftactic.Notations in let trace = push_trace (loc,LtacMLCall tac) ist in let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 54d32f266..1326818fc 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -16,7 +16,6 @@ open Globnames open Term open Genredexpr open Patternops -open Pretyping (** Substitution of tactics at module closing time *) diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 7cda8d914..655bfd5f5 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -10,17 +10,12 @@ open Term open Hipattern open Names open Pp -open Genarg open Geninterp -open Stdarg open Misctypes open Tacexpr open Tacinterp -open Tactics -open Errors open Util open Tacticals.New -open Proofview.Notations let tauto_plugin = "tauto" let () = Mltop.add_known_module tauto_plugin diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index f0c12ab8e..04b622864 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -14,9 +14,7 @@ open Extend open Constrexpr open Notation_term open Libnames -open Tacexpr open Names -open Egramml (**************************************************************************) (* diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 37fccdb3c..95ac87247 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -7,8 +7,6 @@ (************************************************************************) open Util -open Compat -open Names open Extend open Pcoq open Genarg diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 1c39858ea..35ba9757d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -20,7 +20,6 @@ open Misctypes open Tok (* necessary for camlp4 *) open Pcoq -open Pcoq.Tactic open Pcoq.Prim open Pcoq.Constr open Pcoq.Vernac_ diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 53d2089c0..fe9ab630f 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -12,7 +12,6 @@ open Errors open Util open Extend open Genarg -open Tok (* necessary for camlp4 *) (** The parser of Coq *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index c01214377..898dcd255 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -154,11 +154,6 @@ let rec term_equal t1 t2 = open Hashset.Combine -let hash_sorts_family = function -| InProp -> 0 -| InSet -> 1 -| InType -> 2 - let rec hash_term = function | Symb c -> combine 1 (hash_constr c) | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 9a53e2e16..52a135119 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -11,8 +11,6 @@ open Cctac open Stdarg open Constrarg -open Pcoq.Prim -open Pcoq.Constr DECLARE PLUGIN "cc_plugin" diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 802c36109..78a95143d 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Util open Compat open Pp open Decl_expr diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index 35a5a7616..39cad4d03 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -7,8 +7,6 @@ (************************************************************************) open Constrarg -open Pcoq.Prim -open Pcoq.Constr (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 41a068ff3..67c1c5901 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -19,7 +19,6 @@ open Table open Extraction open Modutil open Common -open Mod_subst (***************************************) (*S Part I: computing Coq environment. *) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index ca4e13e12..eb2f02244 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -14,7 +14,6 @@ open Genarg open Stdarg open Constrarg open Pcoq.Prim -open Pcoq.Constr open Pp open Names open Nameops diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index df79c585e..8874afef3 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,8 +1,6 @@ open Pp -open Errors open Util open Names -open Nameops open Globnames open Table open Miniml @@ -18,9 +16,6 @@ let json_int i = let json_bool b = if b then str "true" else str "false" -let json_null = - str "null" - let json_global typ ref = json_str (Common.pp_global typ ref) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index b5e8b4804..bd4831130 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -380,14 +380,6 @@ let rec depcheck_struct = function let lse' = depcheck_se lse in if List.is_empty lse' then struc' else (mp,lse')::struc' -let is_prefix pre s = - let len = String.length pre in - let rec is_prefix_aux i = - if Int.equal i len then true - else pre.[i] == s.[i] && is_prefix_aux (succ i) - in - is_prefix_aux 0 - exception RemainingImplicit of kill_reason let check_for_remaining_implicits struc = diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index b04c4a50c..134b6ba94 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -18,7 +18,6 @@ open Libnames open Constrarg open Stdarg open Pcoq.Prim -open Pcoq.Tactic DECLARE PLUGIN "ground_plugin" diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 0bc40136c..0e2a40245 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -12,7 +12,6 @@ open Errors open Util open Term open Vars -open Glob_term open Tacmach open Tactics open Tacticals @@ -98,8 +97,6 @@ let rec collect_quantified seq= (* open instances processor *) -let dummy_constr=mkMeta (-1) - let dummy_bvid=Id.of_string "x" let mk_open_instance id idc gl m t= diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 8bc84608e..dc5dd45ab 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -16,7 +16,6 @@ open Term open Tactics open Names open Globnames -open Tacmach open Fourier open Contradiction open Proofview.Notations diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 02cd819f4..839586528 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -5,7 +5,6 @@ open Term open Vars open Namegen open Names -open Declarations open Pp open Tacmach open Termops diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 0ba18f568..6dfc23511 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -9,15 +9,12 @@ open Compat open Util open Term -open Vars -open Names open Pp open Constrexpr open Indfun_common open Indfun open Genarg open Constrarg -open Tacticals open Misctypes open Pcoq.Prim open Pcoq.Constr diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 046c7aa43..e98ac5fb5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -208,7 +208,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob (* Debugging mechanism *) let debug_queue = Stack.create () -let rec print_debug_queue b e = +let print_debug_queue b e = if not (Stack.is_empty debug_queue) then begin diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 5fef6d3fc..5c0a8226a 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -18,9 +18,7 @@ open Pp open Mutils -open Proofview open Goptions -open Proofview.Notations (** * Debug flag diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index bca1c2feb..e6b5cc60d 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,12 +16,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Errors -open Misctypes -open Stdarg open Constrarg -open Pcoq.Prim -open Pcoq.Tactic DECLARE PLUGIN "micromega_plugin" diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index b314e0d85..d7538146f 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -20,7 +20,6 @@ DECLARE PLUGIN "omega_plugin" open Names open Coq_omega open Constrarg -open Pcoq.Prim let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index e4c8da93b..fd87d5b7d 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -14,9 +14,6 @@ open Tacexpr open Geninterp open Quote open Constrarg -open Pcoq.Prim -open Pcoq.Constr -open Pcoq.Tactic DECLARE PLUGIN "quote_plugin" diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 61efa9f54..fd4ede6c3 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -13,7 +13,6 @@ DECLARE PLUGIN "romega_plugin" open Names open Refl_omega open Constrarg -open Pcoq.Prim let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 1ebb6e6b7..f5a734048 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -16,7 +16,6 @@ open Newring_ast open Newring open Stdarg open Constrarg -open Pcoq.Prim open Pcoq.Constr open Pcoq.Tactic diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 7ef89b7a0..271bf35a8 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,11 +153,6 @@ let ic_unsafe c = (*FIXME remove *) let sigma = Evd.from_env env in fst (Constrintern.interp_constr env sigma c) -let ty c = - let env = Global.env() in - let sigma = Evd.from_env env in - Typing.unsafe_type_of env sigma c - let decl_constant na ctx c = let vars = Universes.universes_of_constr c in let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in @@ -185,9 +180,6 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args) -let ltac_record flds = - TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds) - let dummy_goal env sigma = let (gl,_,sigma) = Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in @@ -290,8 +282,6 @@ let my_reference c = let new_ring_path = DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) -let ltac s = - lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s)) let znew_ring_path = DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = @@ -318,21 +308,12 @@ let coq_mk_reqe = my_constant "mk_reqe" let coq_semi_ring_theory = my_constant "semi_ring_theory" let coq_mk_seqe = my_constant "mk_seqe" -let ltac_inv_morph_gen = zltac"inv_gen_phi" -let ltac_inv_morphZ = zltac"inv_gen_phiZ" -let ltac_inv_morphN = zltac"inv_gen_phiN" -let ltac_inv_morphNword = zltac"inv_gen_phiNword" let coq_abstract = my_constant"Abstract" let coq_comp = my_constant"Computational" let coq_morph = my_constant"Morphism" -(* morphism *) -let coq_ring_morph = my_constant "ring_morph" -let coq_semi_morph = my_constant "semi_morph" - (* power function *) let ltac_inv_morph_nothing = zltac"inv_morph_nothing" -let coq_pow_N_pow_N = my_constant "pow_N_pow_N" (* hypothesis *) let coq_mkhypo = my_reference "mkhypo" @@ -583,18 +564,6 @@ let dest_ring env sigma th_spec = | _ -> error "bad ring structure" -let dest_morph env sigma m_spec = - let m_typ = Retyping.get_type_of env sigma m_spec in - match kind_of_term m_typ with - App(f,[|r;zero;one;add;mul;sub;opp;req; - c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when eq_constr_nounivs f (Lazy.force coq_ring_morph) -> - (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) - | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when eq_constr_nounivs f (Lazy.force coq_semi_morph) -> - (c,czero,cone,cadd,cmul,None,None,ceqb,phi) - | _ -> error "bad morphism structure" - let reflect_coeff rkind = (* We build an ill-typed terms on purpose... *) match rkind with diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index ef3a3f525..d349cf821 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util open Pp open Names @@ -14,7 +13,6 @@ open Term open Vars open Termops open Namegen -open Pre_env open Environ open Evd open Evarutil diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3d1822102..455a7dbd6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -20,7 +20,6 @@ open Reductionops open Evarutil open Pretype_errors open Sigma.Notations -open Context.Rel.Declaration let normalize_evar evd ev = match kind_of_term (whd_evar evd (mkEvar ev)) with diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 8ddfeaf2f..17bf28793 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -18,7 +18,6 @@ open Inductive open Util open Nativecode open Nativevalues -open Nativelambda open Context.Rel.Declaration (** This module implements normalization by evaluation to OCaml code *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 3a5796fe1..3ff96cd72 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -25,7 +25,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions open Goptions -let set_typeclasses_unique_solutions = +let _ = declare_bool_option { optsync = true; optdepr = false; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f0548238a..10b2bda05 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -99,11 +99,6 @@ module Make | ETBinder false -> str "closed binder" | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" - let strip_meta id = - let s = Id.to_string id in - if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1)) - else id - let pr_comment pr_c = function | CommentConstr c -> pr_c c | CommentString s -> qs s diff --git a/printing/printmod.ml b/printing/printmod.ml index 9354cd28d..5f98eeeab 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,7 +65,6 @@ let get_new_id locals id = (** Inductive declarations *) -open Termops open Reduction let print_params env sigma params = diff --git a/proofs/refine.ml b/proofs/refine.ml index db0b26f7e..76e2d7dc5 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util -open Proofview_monad open Sigma.Notations open Proofview.Notations open Context.Named.Declaration diff --git a/stm/spawned.ml b/stm/spawned.ml index c6df87267..2eae6f5e2 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -13,19 +13,6 @@ let prerr_endline s = if !Flags.debug then begin pr_err s end else () type chandescr = AnonPipe | Socket of string * int * int -let handshake cin cout = - try - match input_value cin with - | Hello(v, pid) when v = proto_version -> - prerr_endline (Printf.sprintf "Handshake with %d OK" pid); - output_value cout (Hello (proto_version,Unix.getpid ())); flush cout - | _ -> raise (Failure "handshake protocol") - with - | Failure s | Invalid_argument s | Sys_error s -> - pr_err ("Handshake failed: " ^ s); raise (Failure "handshake") - | End_of_file -> - pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") - let open_bin_connection h pr pw = let open Unix in let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in diff --git a/stm/stm.ml b/stm/stm.ml index c296361a1..b6ba5815a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1343,7 +1343,6 @@ end = struct (* {{{ *) let set_perspective idl = ProofTask.set_perspective idl; TaskQueue.broadcast (Option.get !queue); - let open Stateid in let open ProofTask in let overlap s1 s2 = List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 950eeef52..6d6e51536 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -15,10 +15,8 @@ open Term open Termops open Errors open Util -open Tacexpr open Mod_subst open Locus -open Sigma.Notations open Proofview.Notations (* Rewriting rules *) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index ab6fb37fd..26166bd83 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,14 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Term open Hipattern open Tactics open Coqlib open Reductionops open Misctypes -open Sigma.Notations open Proofview.Notations open Context.Named.Declaration diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9cfb805d4..6bbd9b2e8 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -17,12 +17,10 @@ open Proof_type open Tacticals open Tacmach open Tactics -open Patternops open Clenv open Auto open Genredexpr open Tacexpr -open Misctypes open Locus open Locusops open Hints @@ -52,16 +50,6 @@ let registered_e_assumption = (Tacmach.New.pf_ids_of_hyps gl)) end } -let eval_uconstrs ist cs = - let flags = { - Pretyping.use_typeclasses = false; - use_unif_heuristics = true; - use_hook = Some Pfedit.solve_by_implicit_tactic; - fail_evar = false; - expand_evars = true - } in - List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs - (************************************************************************) (* PROLOG tactic *) (************************************************************************) @@ -114,7 +102,6 @@ let prolog_tac l n = end open Auto -open Unification (***************************************************************************) (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 011296a8d..ef361d326 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -12,7 +12,6 @@ (* by Eduardo Gimenez *) (************************************************************************) -open Errors open Util open Names open Namegen @@ -27,7 +26,6 @@ open Hipattern open Pretyping open Tacmach.New open Coqlib -open Proofview.Notations (* This file containts the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0bb842601..2fe4d620e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4652,7 +4652,6 @@ let rec shrink ctx sign c t accu = | _ -> assert false let shrink_entry sign const = - let open Context.Named.Declaration in let open Entries in let typ = match const.const_entry_type with | None -> assert false diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 431080c6b..81c01f29d 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -75,7 +75,7 @@ let stop_env () = if !r then stop (); r := false in (fun x -> !r), start_env, stop_env - let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph + let _, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote let url_buffer = Buffer.create 40 @@ -111,12 +111,6 @@ Cdglobals.gallina := s.st_gallina; Cdglobals.light := s.st_light - let without_ref r f x = save_state (); r := false; f x; restore_state () - - let without_gallina = without_ref Cdglobals.gallina - - let without_light = without_ref Cdglobals.light - let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 47acc7b43..9be791a8d 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -77,32 +77,6 @@ let find m l = Hashtbl.find reftable (m, l) let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) -(*s Manipulating path prefixes *) - -type stack = string list - -let rec string_of_stack st = - match st with - | [] -> "" - | x::[] -> x - | x::tl -> (string_of_stack tl) ^ "." ^ x - -let empty_stack = [] - -let module_stack = ref empty_stack -let section_stack = ref empty_stack - -let push st p = st := p::!st -let pop st = - match !st with - | [] -> () - | _::tl -> st := tl - -let head st = - match st with - | [] -> "" - | x::_ -> x - (* Coq modules *) let split_sp s = diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2b2690968..82d3d62b5 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -953,7 +953,7 @@ module TeXmacs = struct (*s Latex preamble *) - let (preamble : string Queue.t) = + let (_ : string Queue.t) = in_doc := false; Queue.create () let header () = @@ -1122,7 +1122,6 @@ module Raw = struct for i = 0 to String.length s - 1 do char s.[i] done let start_module () = () - let end_module () = () let start_latex_math () = () let stop_latex_math () = () diff --git a/toplevel/command.ml b/toplevel/command.ml index 38bc0e568..5865fec06 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -13,7 +13,6 @@ open Flags open Term open Vars open Termops -open Entries open Environ open Redexpr open Declare diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 04182cf23..c6f49dcd4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -9,7 +9,6 @@ open Pp open Errors open Util -open System open Flags open Names open Libnames diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index ffa11679c..6b267283a 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -11,7 +11,6 @@ open Errors open Util open Term open Vars -open Entries open Declarations open Cooking open Entries diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a041ee620..701bc5da5 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -23,7 +23,6 @@ open Vernacexpr open Pcoq open Libnames open Tok -open Egramml open Egramcoq open Notation open Nameops diff --git a/toplevel/record.ml b/toplevel/record.ml index 93429da5a..d12b5ee8e 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -26,7 +26,6 @@ open Constrexpr_ops open Goptions open Sigma.Notations open Context.Rel.Declaration -open Entries (********** definition d'un record (structure) **************) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 89bc31d0a..1c8d60251 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -12,7 +12,6 @@ open Pp open Errors open Util open Flags -open System open Vernacexpr (* The functions in this module may raise (unexplainable!) exceptions. |