Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

still some more dead code removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit 0256a92eb0d0265750bd38a85dce4f9487aefe5b 1 parent 30cf9c6
letouzey authored
Showing with 7 additions and 156 deletions.
  1. +0 −5 checker/check_stat.ml
  2. +0 −1  checker/checker.ml
  3. +0 −1  checker/closure.ml
  4. +1 −2  checker/declarations.ml
  5. +0 −1  checker/mod_checking.ml
  6. +0 −2  checker/modops.ml
  7. +0 −1  checker/reduction.ml
  8. +0 −3  checker/subtyping.ml
  9. +1 −2  checker/term.ml
  10. +1 −1  checker/typeops.ml
  11. +1 −1  checker/validate.ml
  12. +0 −8 dev/top_printers.ml
  13. +0 −1  parsing/lexer.ml4
  14. +0 −19 plugins/funind/functional_principles_types.ml
  15. +1 −2  plugins/micromega/csdpcert.ml
  16. +2 −2 plugins/micromega/sos_lib.ml
  17. +0 −6 plugins/xml/xmlcommand.ml
  18. +0 −12 printing/pptactic.ml
  19. +0 −4 printing/ppvernac.ml
  20. +0 −9 proofs/proof_global.ml
  21. +0 −1  proofs/proof_type.ml
  22. +0 −2  tactics/auto.ml
  23. +0 −1  tactics/elim.ml
  24. +0 −2  tactics/hiddentac.ml
  25. +0 −13 tools/coqdoc/cpretty.mll
  26. +0 −35 tools/coqdoc/index.ml
  27. +0 −7 tools/coqdoc/output.ml
  28. +0 −2  tools/coqdoc/tokens.ml
  29. +0 −1  tools/coqwc.mll
  30. +0 −1  tools/gallina_lexer.mll
  31. +0 −1  toplevel/metasyntax.ml
  32. +0 −7 toplevel/toplevel.ml
View
5 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
View
1  checker/checker.ml
@@ -12,7 +12,6 @@ open Util
open System
open Flags
open Names
-open Term
open Check
let () = at_exit flush_all
View
1  checker/closure.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
open Util
open Pp
open Term
View
3  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
View
1  checker/mod_checking.ml
@@ -4,7 +4,6 @@ open Errors
open Util
open Names
open Term
-open Inductive
open Reduction
open Typeops
open Indtypes
View
2  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 =
View
1  checker/reduction.ml
@@ -8,7 +8,6 @@
open Errors
open Util
-open Names
open Term
open Univ
open Closure
View
3  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
View
3  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
View
2  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
View
2  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;
View
8 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 =
View
1  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} *)
View
19 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
View
3  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)
View
4 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 =
View
6 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
View
12 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
View
4 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
View
9 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
View
1  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
View
2  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
View
1  tactics/elim.ml
@@ -16,7 +16,6 @@ open Hipattern
open Tacmach
open Tacticals
open Tactics
-open Tacexpr
open Misctypes
let introElimAssumsThen tac ba =
View
2  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
View
13 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;
View
35 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
View
7 tools/coqdoc/output.ml
@@ -581,9 +581,6 @@ module Html = struct
| '&' -> printf "&amp;"
| 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"
View
2  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.
View
1  tools/coqwc.mll
@@ -15,7 +15,6 @@
(*i*){
open Printf
open Lexing
-open Filename
(*i*)
(*s Command-line options. *)
View
1  tools/gallina_lexer.mll
@@ -7,7 +7,6 @@
(************************************************************************)
{
- open Lexing
let chan_out = ref stdout
View
1  toplevel/metasyntax.ml
@@ -8,7 +8,6 @@
open Pp
open Flags
-open Compat
open Errors
open Util
open Names
View
7 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
Please sign in to comment.
Something went wrong with that request. Please try again.