Permalink
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...
1 parent 30cf9c6 commit 0256a92eb0d0265750bd38a85dce4f9487aefe5b letouzey committed Oct 6, 2012
View
@@ -7,12 +7,7 @@
(************************************************************************)
open Pp
-open Errors
-open Util
-open System
-open Flags
open Names
-open Term
open Declarations
open Environ
View
@@ -12,7 +12,6 @@ open Util
open System
open Flags
open Names
-open Term
open Check
let () = at_exit flush_all
View
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
open Util
open Pp
open Term
View
@@ -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
@@ -4,7 +4,6 @@ open Errors
open Util
open Names
open Term
-open Inductive
open Reduction
open Typeops
open Indtypes
View
@@ -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
@@ -8,7 +8,6 @@
open Errors
open Util
-open Names
open Term
open Univ
open Closure
View
@@ -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
@@ -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
@@ -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
@@ -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,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
@@ -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} *)
@@ -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
@@ -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)
@@ -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 =
@@ -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
@@ -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
@@ -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
@@ -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
@@ -12,7 +12,6 @@ open Names
open Term
open Tacexpr
open Glob_term
-open Genarg
open Nametab
open Pattern
open Misctypes
View
@@ -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
@@ -16,7 +16,6 @@ open Hipattern
open Tacmach
open Tacticals
open Tactics
-open Tacexpr
open Misctypes
let introElimAssumsThen tac ba =
View
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Refiner
-open Tacexpr
open Tactics
open Util
open Locus
View
@@ -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;
Oops, something went wrong.

0 comments on commit 0256a92

Please sign in to comment.