diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 4 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 3 | ||||
| -rw-r--r-- | parsing/vernacextend.ml4 | 3 |
5 files changed, 0 insertions, 19 deletions
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 |