Permalink
Browse files

Remove some dead-code (thanks to ocaml warnings)

 The removed code isn't used locally and isn't exported in the signature
  • Loading branch information...
1 parent adfd437 commit 8fc2509f354b02ec4e0a3eb6fabc329109686c47 @letouzey letouzey committed Mar 5, 2014
View
@@ -122,9 +122,3 @@ let revert_reserved_type t =
with Not_found | Failure _ -> Anonymous
let _ = Namegen.set_reserved_typed_name revert_reserved_type
-
-let default_env () = {
- ninterp_var_type = Id.Map.empty;
- ninterp_rec_vars = Id.Map.empty;
- ninterp_only_parse = false;
-}
View
@@ -325,8 +325,6 @@ let map f c = match kind c with
if tl'==tl && bl'==bl then c
else mkCoFix (ln,(lna,tl',bl'))
-exception Exit of int * constr
-
(* [map_with_binders 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 [n]) at
View
@@ -82,8 +82,6 @@ let update_case_info cache ci modlist =
with Not_found ->
ci
-let empty_modlist = (Cmap.empty, Mindmap.empty)
-
let is_empty_modlist (cm, mm) =
Cmap.is_empty cm && Mindmap.is_empty mm
View
@@ -431,7 +431,6 @@ module KerPair = struct
| Dual (kn,_) -> kn
let same kn = Same kn
- let dual knu knc = Dual (knu,knc)
let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
let make1 = same
@@ -726,7 +725,6 @@ let label = KerName.label
let string_of_kn = KerName.to_string
let pr_kn = KerName.print
let kn_ord = KerName.compare
-let kn_equal = KerName.equal
(** Compatibility layer for [Constant] *)
@@ -23,10 +23,6 @@ open Environ
open Entries
open Typeops
-let debug = false
-let prerr_endline =
- if debug then prerr_endline else fun _ -> ()
-
let constrain_type env j cst1 = function
| `None ->
make_polymorphic_if_constant_for_ind env j, cst1
View
@@ -104,7 +104,7 @@ let lift n = liftn n 1
type info = Closed | Open | Unknown
type 'a substituend = { mutable sinfo: info; sit: 'a }
-let rec lift_substituend depth s =
+let lift_substituend depth s =
match s.sinfo with
| Closed -> s.sit
| Open -> lift depth s.sit
View
@@ -306,8 +306,6 @@ let subtract cmp l1 l2 =
let unionq l1 l2 = union (==) l1 l2
let subtractq l1 l2 = subtract (==) l1 l2
-let tabulate = init
-
let interval n m =
let rec interval_n (l,m) =
if n > m then l else interval_n (m::l, pred m)
View
@@ -19,17 +19,9 @@ exception Anomaly of string option * std_ppcmds (* System errors *)
let make_anomaly ?label pp =
Anomaly (label, pp)
-let anomaly_gen label pp =
- raise (Anomaly (label, pp))
-
-let anomaly ?loc ?label pp =
- match loc with
+let anomaly ?loc ?label pp = match loc with
| None -> raise (Anomaly (label, pp))
- | Some loc ->
- Loc.raise loc (Anomaly (label, pp))
-
-let anomalylabstrm string pps =
- anomaly_gen (Some string) pps
+ | Some loc -> Loc.raise loc (Anomaly (label, pp))
let is_anomaly = function
| Anomaly _ -> true
@@ -106,8 +98,6 @@ let print e =
isn't printed (used in Ltac debugging). *)
let print_no_report e = print_gen (print_anomaly false) !handle_stack e
-let print_anomaly e = print_anomaly true e
-
(** Predefined handlers **)
let _ = register_handler begin function
View
@@ -179,14 +179,6 @@ let is_standard_doc_url url =
url = Coq_config.wwwrefman ||
url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
-(* same as in System, but copied here because of dependencies *)
-let canonical_path_name p =
- let current = Sys.getcwd () in
- Sys.chdir p;
- let result = Sys.getcwd () in
- Sys.chdir current;
- result
-
(* Options for changing coqlib *)
let coqlib_spec = ref false
let coqlib = ref "(not initialized yet)"
View
@@ -154,10 +154,6 @@ let has_type (t, v) u = argument_type_eq t u
let unquote x = x
-type an_arg_of_this_type = Obj.t
-
-let in_generic t x = (t, Obj.repr x)
-
type ('a,'b) abstract_argument_type = argument_type
type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
@@ -237,7 +233,7 @@ struct
(** For now, the following function is quite dummy and should only be applied
to an extra argument type, otherwise, it will badly fail. *)
- let rec obj t = match t with
+ let obj t = match t with
| ExtraArgType s -> Obj.magic (get_obj0 s)
| _ -> assert false
View
@@ -452,8 +452,6 @@ struct
let get = M.get
-let set = M.set
-
let of_array (t : 'a array) : 'a M.t =
let tag = Obj.tag (Obj.repr t) in
let () = if tag = Obj.double_array_tag then
View
@@ -26,7 +26,7 @@ let rec force s = match Lazy.force s with
let force s = force s; s
-let rec is_empty s = match Lazy.force s with
+let is_empty s = match Lazy.force s with
| Nil -> true
| Cons (_, _) -> false
View
@@ -49,7 +49,6 @@ module List = struct
end
let min (i : int) j = if i < j then i else j
-let max (i : int) j = if i > j then i else j
(** Utility function *)
let rec next from upto =
@@ -83,7 +82,7 @@ struct
let reroot t = rerootk t (fun () -> ())
- let rec get t i =
+ let get t i =
let () = assert (0 <= i) in
match !t with
| Root a ->
View
@@ -25,10 +25,6 @@ exception Marshal_error
(** Utility functions *)
-let rec has_flag (f : string) = function
- | [] -> false
- | (k, _) :: l -> CString.equal k f || has_flag f l
-
let rec get_attr attr = function
| [] -> raise Not_found
| (k, v) :: l when CString.equal k attr -> v
@@ -186,13 +182,6 @@ let to_state_id xml =
let of_edit_or_state_id = function
| Interface.Edit id -> ["object","edit"], of_edit_id id
| Interface.State id -> ["object","state"], of_state_id id
-let to_edit_or_state_id attrs xml =
- try
- let obj = get_attr "object" attrs in
- if obj = "edit"then Interface.Edit (to_edit_id xml)
- else if obj = "state" then Interface.State (to_state_id xml)
- else raise Marshal_error
- with Not_found -> raise Marshal_error
let of_value f = function
| Good x -> Element ("value", ["val", "good"], [f x])
@@ -410,7 +399,6 @@ module ReifType : sig (* {{{ *)
type value_type
val erase : 'a val_t -> value_type
val print_type : value_type -> string
- val same_type : 'a val_t -> value_type -> bool
val document_type_encoding : (xml -> string) -> unit
@@ -432,7 +420,6 @@ end = struct
type 'a val_t = value_type
let erase (x : 'a val_t) : value_type = x
- let same_type (x : 'a val_t) (y : value_type) = Pervasives.compare (erase x) y = 0
let unit_t = Unit
let string_t = String
View
@@ -52,8 +52,6 @@ let labels (Node (_,m)) =
(** FIXME: this is order-dependent. Try to find a more robust presentation? *)
List.rev (T_codom.fold (fun x _ acc -> x::acc) m [])
-let in_dom (Node (_,m)) lbl = T_codom.mem lbl m
-
let is_empty_node (Node(a,b)) = (X.is_nil a) && (T_codom.is_empty b)
let assure_arc m lbl =
@@ -138,7 +138,6 @@ let iter_ref () =
let iter = function () -> (constr_of_global (delayed_force iter_ref))
let eq = function () -> (coq_base_constant "eq")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let acc_intro_generator_function = function () -> (constant ["Recdef"] "Acc_intro_generator_function")
let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm")
let le_trans = function () -> (coq_base_constant "le_trans")
let le_lt_trans = function () -> (coq_base_constant "le_lt_trans")
@@ -163,8 +163,6 @@ let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
(* equality between polynomials *)
-exception Failed
-
let rec equal p q =
match (p,q) with
(Pint a,Pint b) -> C.equal a b
@@ -768,10 +768,6 @@ let filter_candidates evd evk filter candidates =
let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in
Some (List.filter (fun a -> Id.Set.subset (collect_vars a) ids) l)
-let eq_filter f1 f2 =
- let eq_bool b1 b2 = if b1 then b2 else not b2 in
- List.equal eq_bool f1 f2
-
let closure_of_filter evd evk = function
| None -> None
| Some filter ->
View
@@ -176,41 +176,6 @@ let new_meta =
let mk_new_meta () = mkMeta(new_meta())
-(** Transfer an evar from [sigma2] to [sigma1] *)
-let transfer ev (sigma1, sigma2) =
- let nsigma1 = Evd.add sigma1 ev (Evd.find sigma2 ev) in
- let nsigma2 = Evd.remove sigma2 ev in
- (nsigma1, nsigma2)
-
-let collect_evars emap c =
- let rec collrec acc c =
- match kind_of_term c with
- | Evar (evk,_) ->
- if Evd.is_undefined emap evk then Evar.Set.add evk acc
- else (* No recursion on the evar instantiation *) acc
- | _ ->
- fold_constr collrec acc c in
- collrec Evar.Set.empty c
-
-let push_dependent_evars sigma emap =
- let fold ev {evar_concl = ccl} (sigma, emap) =
- Evar.Set.fold transfer (collect_evars emap ccl) (sigma, emap)
- in
- Evd.fold_undefined fold emap (sigma, emap)
-
-let push_duplicated_evars sigma emap c =
- let rec collrec (one, evars as acc) c =
- match kind_of_term c with
- | Evar (evk,_) when not (Evd.mem (fst evars) evk) ->
- if List.exists (fun ev -> Evar.equal evk ev) one then
- (one, transfer evk evars)
- else
- (evk::one, evars)
- | _ ->
- fold_constr collrec acc c
- in
- snd (collrec ([],(sigma,emap)) c)
-
(* The list of non-instantiated existential declarations (order is important) *)
let non_instantiated sigma =
@@ -221,8 +186,6 @@ let non_instantiated sigma =
(* Manipulating filters *)
(************************)
-let extract_subfilter = List.filter_with
-
let make_pure_subst evi args =
snd (List.fold_right
(fun (id,b,c) (args,l) ->
@@ -492,7 +492,7 @@ let apply_subst recfun env cst_l t stack =
| _ -> recfun cst_l (substl env t, stack)
in aux env cst_l t stack
-let rec stacklam recfun env t stack =
+let stacklam recfun env t stack =
apply_subst (fun _ -> recfun) env [] t stack
let beta_applist (c,l) =
@@ -48,7 +48,7 @@ let unsatisfiable_constraints env evd ev comp =
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
-let rec unsatisfiable_exception exn =
+let unsatisfiable_exception exn =
match exn with
| TypeClassError (_, UnsatisfiableConstraints _) -> true
| _ -> false
@@ -286,8 +286,6 @@ let pr_raw_alias prc prlc prtac prpat =
pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
let pr_glob_alias prc prlc prtac prpat =
pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
-let pr_alias prc prlc prtac prpat =
- pr_extend_gen (pr_top_generic prc prlc prtac prpat)
(**********************************************************************)
(* The tactic printer *)
@@ -1025,9 +1023,6 @@ let pr_glob_tactic env = pr_glob_tactic_level env ltop
(** Registering *)
-let register_uniform_printer wit pr =
- Genprint.register_print0 wit pr pr pr
-
let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
View
@@ -130,17 +130,7 @@ let pr_search a b pr_p = match a with
| SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| SearchAbout sl -> str"Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
-let pr_locality_full = function
- | None -> mt ()
- | Some true -> str "Local" ++ spc ()
- | Some false -> str "Global "++ spc ()
-
let pr_locality local = if local then str "Local" ++ spc () else mt ()
-let pr_non_locality local = if local then mt () else str "Global" ++ spc ()
-let pr_section_locality local =
- if Lib.sections_are_opened () && not local then str "Global "
- else if not (Lib.sections_are_opened ()) && local then str "Local "
- else mt ()
let pr_explanation (e,b,f) =
let a = match e with
View
@@ -720,11 +720,6 @@ let pr_assumptionset env s =
] in
prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
-open Typeclasses
-
-let pr_instance i =
- pr_global (instance_impl i)
-
(** Inductive declarations *)
open Termops
View
@@ -57,7 +57,7 @@ let is_unification_error = function
| UnsolvableImplicit _| AbstractionOverMeta _ -> true
| _ -> false
-let rec catchable_exception = function
+let catchable_exception = function
| Errors.UserError _ | TypeError _
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _
View
@@ -25,9 +25,6 @@ let delete_proof = Proof_global.discard
let delete_current_proof = Proof_global.discard_current
let delete_all_proofs = Proof_global.discard_all
-let set_undo _ = ()
-let get_undo _ = None
-
let start_proof (id : Id.t) str hyps c ?init_tac terminator =
let goals = [ (Global.env_of_context hyps , c) ] in
Proof_global.start_proof id str goals terminator;
@@ -132,11 +129,6 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
delete_current_proof ();
raise reraise
-let constr_of_def = function
- | Declarations.Undef _ -> assert false
- | Declarations.Def cs -> Mod_subst.force_constr cs
- | Declarations.OpaqueDef lc -> Opaqueproof.force_proof lc
-
let build_by_tactic env typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
Oops, something went wrong.

0 comments on commit 8fc2509

Please sign in to comment.