Removing dead code, thanks to new OCaml warnings and a bit of scripting.

4 files changed, 0 insertions, 28 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 10c3092b47..0186b08ac7 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -102,10 +102,6 @@ let process_vernac_interp_error exn = match exn with
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	 spc () ++ str "was not found" ++
 	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
-  | Nametab.GlobalizationConstantError q ->
-      wrap_vernac_error exn
-        (str "No constant of this name:" ++ spc () ++
-         Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
       let s = Lazy.force s in
       wrap_vernac_error exn
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 954d754937..51dc8d5bbd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -73,8 +73,6 @@ let outputstate = ref ""
 let set_outputstate s = outputstate:=s
 let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
 
-let set_default_include d =
-  push_include d Nameops.default_root_prefix false false
 let set_include d p recursive implicit =
   let p = dirpath_of_string p in
   push_include d p recursive implicit
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b2f752dce9..fd74f9c06d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1064,23 +1064,6 @@ let explain_wrong_numarg_inductive env ind n =
   str "The inductive type " ++ pr_inductive env ind ++
   str " expects " ++ str (decline_string n "argument") ++ str "."
 
-let explain_wrong_predicate_arity env pred nondep_arity dep_arity=
-  let env = make_all_name_different env in
-  let pp = pr_lconstr_env env pred in
-  str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++
-  str "should be of arity" ++ spc () ++
-  pr_lconstr_env env nondep_arity ++ spc () ++
-  str "(for non dependent case) or" ++
-  spc () ++ pr_lconstr_env env dep_arity ++ spc () ++
-  str "(for dependent case)."
-
-let explain_needs_inversion env x t =
-  let env = make_all_name_different env in
-  let px = pr_lconstr_env env x in
-  let pt = pr_lconstr_env env t in
-  str "Sorry, I need inversion to compile pattern matching on term " ++
-  px ++ str " of type: " ++ pt ++ str "."
-
 let explain_unused_clause env pats =
 (* Without localisation
   let s = if List.length pats > 1 then "s" else "" in
@@ -1112,10 +1095,6 @@ let explain_pattern_matching_error env = function
       explain_wrong_numarg_constructor env c n
   | WrongNumargInductive (c,n) ->
       explain_wrong_numarg_inductive env c n
-  | WrongPredicateArity (pred,n,dep) ->
-      explain_wrong_predicate_arity env pred n dep
-  | NeedsInversion (x,t) ->
-      explain_needs_inversion env x t
   | UnusedClause tms ->
       explain_unused_clause env tms
   | NonExhaustive tms ->
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index fc52d36443..875c933efa 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -332,7 +332,6 @@ end = struct (* {{{ *)
   let current_branch () = current_branch !vcs
 
   let checkout head = vcs := checkout !vcs head
-  let master = Branch.master
   let branches () = branches !vcs
   let get_branch head = get_branch !vcs head
   let get_branch_pos head = (get_branch head).pos