diff options
32 files changed, 7 insertions, 156 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 0e7aec1a8..3176a4307 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -7,12 +7,7 @@ (************************************************************************) open Pp -open Errors -open Util -open System -open Flags open Names -open Term open Declarations open Environ diff --git a/checker/checker.ml b/checker/checker.ml index ea2e3892f..8389803fc 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -12,7 +12,6 @@ open Util open System open Flags open Names -open Term open Check let () = at_exit flush_all diff --git a/checker/closure.ml b/checker/closure.ml index f86aa82eb..c515bdb24 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util open Pp open Term diff --git a/checker/declarations.ml b/checker/declarations.ml index 8b146d18b..df0134e02 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -1,4 +1,3 @@ -open Errors open Util open Names open Term @@ -111,7 +110,7 @@ let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst let mp_in_delta mp = Deltamap.mem_mp mp -let rec find_prefix resolve mp = +let find_prefix resolve mp = let rec sub_mp = function | MPdot(mp,l) as mp_sup -> (try Deltamap.find_mp mp_sup resolve diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index a51b66ce0..7dfa29e16 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -4,7 +4,6 @@ open Errors open Util open Names open Term -open Inductive open Reduction open Typeops open Indtypes diff --git a/checker/modops.ml b/checker/modops.ml index 9d5829605..1c4a2916e 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -11,10 +11,8 @@ open Errors open Util open Pp open Names -open Univ open Term open Declarations -open Environ (*i*) let error_not_a_constant l = diff --git a/checker/reduction.ml b/checker/reduction.ml index 195f7d423..c2d5c261c 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -8,7 +8,6 @@ open Errors open Util -open Names open Term open Univ open Closure diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 7d2ced7fd..390c2b9e7 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -18,9 +18,6 @@ open Reduction open Inductive open Modops (*i*) -open Pp - - (* This local type is used to subtype a constant with a constructor or an inductive type. It can also be useful to allow reorderings in diff --git a/checker/term.ml b/checker/term.ml index b41bebca2..0c3fc741d 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -10,7 +10,6 @@ open Errors open Util -open Pp open Names open Univ open Esubst @@ -134,7 +133,7 @@ let rec strip_outer_cast c = match c with | Cast (c,_,_) -> strip_outer_cast c | _ -> c -let rec collapse_appl c = match c with +let collapse_appl c = match c with | App (f,cl) -> let rec collapse_rec f cl2 = match (strip_outer_cast f) with diff --git a/checker/typeops.ml b/checker/typeops.ml index 91f58a04a..ad05f96b7 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -75,7 +75,7 @@ let judge_of_variable env id = (* Checks if a context of variable can be instantiated by the variables of the current env *) (* TODO: check order? *) -let rec check_hyps_inclusion env sign = +let check_hyps_inclusion env sign = fold_named_context (fun (id,_,ty1) () -> let ty2 = named_type id env in diff --git a/checker/validate.ml b/checker/validate.ml index 2f46695cd..eeff9d1cd 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -164,7 +164,7 @@ let val_set ?(name="Set.t") f = vset;ext "bal" val_int|]|]) (* Maps *) -let rec val_map ?(name="Map.t") fk fv = +let val_map ?(name="Map.t") fk fv = val_rec_sum name 1 (fun vmap -> [|[|vmap; ext "key" fk; ext "value" fv; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8e7a92a8f..20e0fff55 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -8,25 +8,19 @@ (* Printers for the ocaml toplevel. *) -open System -open Errors open Util open Pp open Names open Libnames open Globnames open Nameops -open Sign open Univ open Environ open Printer open Term -open Termops -open Cerrors open Evd open Goptions open Genarg -open Mod_subst open Clenv let _ = Constrextern.print_evar_arguments := true @@ -411,7 +405,6 @@ END open Pcoq open Genarg open Egramml -open Egramcoq let _ = try @@ -449,7 +442,6 @@ let _ = (* Setting printer of unbound global reference *) open Names -open Nameops open Libnames let encode_path loc prefix mpdir suffix id = diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index ca5c20c71..3071e0eb4 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -541,7 +541,6 @@ let current_location_table = ref (loct_create ()) type location_table = (int, CompatLoc.t) Hashtbl.t let location_table () = !current_location_table let restore_location_table t = current_location_table := t -let location_function n = loct_func !current_location_table n (** {6 The lexer of Coq} *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a14b47393..533fbfaaa 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -15,25 +15,6 @@ open Misctypes exception Toberemoved_with_rel of int*constr exception Toberemoved - -let pr_elim_scheme el = - let env = Global.env () in - let msg = str "params := " ++ Printer.pr_rel_context env el.params in - let env = Environ.push_rel_context el.params env in - let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in - let env = Environ.push_rel_context el.predicates env in - let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in - let env = Environ.push_rel_context el.branches env in - let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in - let env = Environ.push_rel_context el.args env in - msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl - - -let observe s = - if do_observe () - then Pp.msg_debug s - - let pr_elim_scheme el = let env = Global.env () in let msg = str "params := " ++ Printer.pr_rel_context env el.params in diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index e416c514c..f848591cc 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -12,7 +12,6 @@ (* *) (************************************************************************) -open Big_int open Num open Sos open Sos_types @@ -60,7 +59,7 @@ open Mutils -let rec canonical_sum_to_string = function s -> failwith "not implemented" +let canonical_sum_to_string = function s -> failwith "not implemented" let print_canonical_sum m = Format.print_string (canonical_sum_to_string m) diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index e592611ac..41cbeda3f 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -6,7 +6,7 @@ (* independent bits *) (* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) -open Sos_types + open Num let debugging = ref false;; @@ -546,7 +546,7 @@ let fix err prs input = try prs input with Noparse -> failwith (err ^ " expected");; -let rec listof prs sep err = +let listof prs sep err = prs ++ many (sep ++ fix err prs >> snd) >> (fun (h,t) -> h::t);; let possibly prs input = diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 0673e79fb..8259266af 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -108,12 +108,6 @@ let types_filename_of_filename = | None -> None ;; -let prooftree_filename_of_filename = - function - Some f -> Some (f ^ ".proof_tree") - | None -> None -;; - let theory_filename xml_library_root = let module N = Names in match xml_library_root with diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 48a59be05..2ec66bb34 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -980,15 +980,6 @@ let strip_prod_binders_glob_constr n (ty,_) = | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty -let strip_prod_binders_constr n ty = - let rec strip_ty acc n ty = - if n=0 then (List.rev acc, ty) else - match Term.kind_of_term ty with - Term.Prod(na,a,b) -> - strip_ty (([Loc.ghost,na],a)::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in - strip_ty [] n ty - let drop_env f _env = f let pr_constr_or_lconstr_pattern_expr b = @@ -1030,9 +1021,6 @@ let rec glob_printers = and pr_glob_tactic_level env n (t:glob_tactic_expr) = fst (make_pr_tac glob_printers env) n t -let pr_constr_or_lconstr_pattern b = - if b then pr_lconstr_pattern else pr_constr_pattern - let pr_raw_tactic env = pr_raw_tactic_level env ltop let pr_glob_tactic env = pr_glob_tactic_level env ltop diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3553373fb..686d2ae2d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -175,10 +175,6 @@ let pr_set_option a b = let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)" -let pr_destruct_location = function - | Tacexpr.ConclLocation () -> str"Conclusion" - | Tacexpr.HypLocation b -> if b then str"Discardable Hypothesis" else str"Hypothesis" - let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 178c2ab2d..25ed1f3e8 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -125,15 +125,6 @@ let find_top l = | np::_ -> np | [] -> raise NoCurrentProof -let rotate_top l1 l2 = - let np = extract_top l1 in - push np l2 - -let rotate_find id l1 l2 = - let np = extract id l1 in - push np l2 - - (* combinators for the proof_info map *) let add id info m = m := Idmap.add id info !m diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index e09d72e47..b7237f1fc 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -12,7 +12,6 @@ open Names open Term open Tacexpr open Glob_term -open Genarg open Nametab open Pattern open Misctypes diff --git a/tactics/auto.ml b/tactics/auto.ml index d773d2092..47b89e9af 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1430,6 +1430,4 @@ let gen_auto ?(debug=Off) n lems dbnames = | None -> full_auto ~debug n lems | Some l -> auto ~debug n lems l -let inj_or_var = Option.map (fun n -> ArgArg n) - let h_auto ?(debug=Off) n lems l = gen_auto ~debug n lems l diff --git a/tactics/elim.ml b/tactics/elim.ml index 685a70bad..88348206b 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -16,7 +16,6 @@ open Hipattern open Tacmach open Tacticals open Tactics -open Tacexpr open Misctypes let introElimAssumsThen tac ba = diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index fc0f24fcd..e61922d07 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Refiner -open Tacexpr open Tactics open Util open Locus diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index d7b54fd0f..2c58a05e2 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -75,7 +75,6 @@ let brackets = ref 0 let comment_level = ref 0 let in_proof = ref None - let in_emph = ref false let in_env start stop = let r = ref false in @@ -102,8 +101,6 @@ let length_skip = 1 + String.length s1 in lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip - let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false - (* saving/restoring the PP state *) type state = { @@ -127,8 +124,6 @@ let without_light = without_ref Cdglobals.light - let show_all f = without_gallina (without_light f) - let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () @@ -251,14 +246,6 @@ with _ -> () - let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:=" - let extract_ident s = - assert (String.length s >= 3); - if Str.string_match extract_ident_re s 0 then - Str.matched_group 1 s - else - String.sub s 1 (String.length s - 3) - let output_indented_keyword s lexbuf = let nbsp,isp = count_spaces s in Output.indentation nbsp; diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index d319ce72d..610fa28f7 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Filename -open Lexing open Printf open Cdglobals @@ -37,7 +35,6 @@ type index_entry = | Ref of coq_module * string * entry_type | Mod of coq_module * string -let current_type : entry_type ref = ref Library let current_library = ref "" (** refers to the file being parsed *) @@ -71,10 +68,6 @@ let add_ref m loc m' sp id ty = if Hashtbl.mem deftable idx then () else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty)) -let add_mod m loc m' id = - Hashtbl.add reftable (m, loc) (Mod (m', id)); - Hashtbl.add deftable m (Mod (m', id)) - let find m l = Hashtbl.find reftable (m, l) let find_string m s = Hashtbl.find deftable s @@ -94,9 +87,6 @@ let empty_stack = [] let module_stack = ref empty_stack let section_stack = ref empty_stack -let init_stack () = - module_stack := empty_stack; section_stack := empty_stack - let push st p = st := p::!st let pop st = match !st with @@ -108,27 +98,6 @@ let head st = | [] -> "" | x::_ -> x -let begin_module m = push module_stack m -let begin_section s = push section_stack s - -let end_block id = - (** determines if it ends a module or a section and pops the stack *) - if ((String.compare (head !module_stack) id ) == 0) then - pop module_stack - else if ((String.compare (head !section_stack) id) == 0) then - pop section_stack - else - () - -let make_fullid id = - (** prepends the current module path to an id *) - let path = string_of_stack !module_stack in - if String.length path > 0 then - path ^ "." ^ id - else - id - - (* Coq modules *) let split_sp s = @@ -207,10 +176,6 @@ let sort_entries el = let display_letter c = if c = '*' then "other" else String.make 1 c -let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0 - -let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h [] - let type_name = function | Library -> let ln = !lib_name in diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 86a5b0cbe..a0f36d9a1 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -581,9 +581,6 @@ module Html = struct | '&' -> printf "&" | c -> output_char c - let raw_string s = - for i = 0 to String.length s - 1 do char s.[i] done - let escaped = let buff = Buffer.create 5 in fun s -> @@ -944,8 +941,6 @@ module TeXmacs = struct let (preamble : string Queue.t) = in_doc := false; Queue.create () - let push_in_preamble s = Queue.add s preamble - let header () = output_string "(*i This file has been automatically generated with the command \n"; @@ -1066,8 +1061,6 @@ module TeXmacs = struct let paragraph () = printf "\n\n" - let line_break_true () = printf "<format|line break>" - let line_break () = printf "\n" let empty_line_of_code () = printf "\n" diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index 10a105f9b..7c6c1f092 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -9,8 +9,6 @@ (* Application of printing rules based on a dictionary specific to the target language *) -open Cdglobals - (*s Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. diff --git a/tools/coqwc.mll b/tools/coqwc.mll index a5376ec44..50f989e7c 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -15,7 +15,6 @@ (*i*){ open Printf open Lexing -open Filename (*i*) (*s Command-line options. *) diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll index cfbfac98f..5d8a1d209 100644 --- a/tools/gallina_lexer.mll +++ b/tools/gallina_lexer.mll @@ -7,7 +7,6 @@ (************************************************************************) { - open Lexing let chan_out = ref stdout diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a67400788..e7c19fbb2 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -8,7 +8,6 @@ open Pp open Flags -open Compat open Errors open Util open Names diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7e301ba0e..ec390683f 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -182,13 +182,6 @@ let print_location_in_file s inlibrary fname loc = (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) -let print_command_location ib dloc = - match dloc with - | Some (bp,ep) -> - (str"Error during interpretation of command:" ++ fnl () ++ - str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ()) - | None -> (mt ()) - let valid_loc dloc loc = loc <> Loc.ghost & match dloc with |