From f8b5525eea31c226dfb2ebdc22be512f8af2ebbe Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 8 Apr 2009 17:23:13 +0000
Subject: Some dead code removal + cleanups

  This commit concerns about the first half of the useless code
  mentionned by Oug for coqtop (without plugins). For the moment,
  Oug is used in a mode where any elements mentionned in a .mli
  is considered to be precious. This already allows to detect and
  remove about 600 lines, and more is still to come.

  Among the interesting points, the type Entries.specification_entry
  and its constructors SPExxx were never used. Large parts of cases.ml
  (and hence subtac_cases.ml) were also useless.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constr.ml4     | 4 ----
 parsing/g_vernac.ml4     | 5 -----
 parsing/g_xml.ml4        | 4 ----
 parsing/tacextend.ml4    | 3 ---
 parsing/vernacextend.ml4 | 3 ---
 5 files changed, 19 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 66fc4c2532..8db62c3928 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -33,10 +33,6 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
-let mk_lam = function
-    ([],c) -> c
-  | (bl,c) -> CLambdaN(constr_loc c, bl,c)
-
 let loc_of_binder_let = function
   | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
   | LocalRawDef ((loc,_),_)::_ -> loc
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ec1e7415bc..f656fb32e2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -120,11 +120,6 @@ let test_plurial_form = function
    "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
   | _ -> ()
 
-let no_coercion loc (c,x) =
-  if c then Util.user_err_loc
-    (loc,"no_coercion",str"No coercion allowed here.");
-  x
-
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 3a57fd545d..8142368358 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -71,10 +71,6 @@ let error_expect_no_argument loc =
 let nmtoken (loc,a) =
   try int_of_string a
   with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
-  
-let interp_xml_attr_qualid = function
-  | "uri", s -> qualid_of_string s
-  | _ -> error "Ill-formed xml attribute"
 
 let get_xml_attr s al = 
   try List.assoc s al
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 65b3a075ec..03c7047588 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -16,9 +16,6 @@ open Q_util
 open Q_coqast
 open Argextend
 
-let loc = Util.dummy_loc
-let default_loc = <:expr< Util.dummy_loc >>
-
 type grammar_tactic_production_expr =
   | TacTerm of string
   | TacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index f661800a15..dd6b9e8bf6 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -16,9 +16,6 @@ open Q_util
 open Q_coqast
 open Argextend
 
-let loc = Util.dummy_loc
-let default_loc = <:expr< Util.dummy_loc >>
-
 type grammar_tactic_production_expr =
   | VernacTerm of string
   | VernacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option
-- 
cgit v1.2.3