From 93642cdc3acb9f4e8d1b4ac1f1621d1104f04e54 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 23 Jun 2006 10:03:54 +0000 Subject: Suppresion redondance interp_entry_name entre Q_util et Argextend git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8976 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/argextend.ml4 | 35 ----------------------------------- 1 file changed, 35 deletions(-) (limited to 'parsing/argextend.ml4') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index a4239713b..07c1470c9 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -176,41 +176,6 @@ let declare_vernac_argument loc s cl = open Vernacexpr open Pcoq - -let rec interp_entry_name loc s = - let l = String.length s in - if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in - List1ArgType t, <:expr< Gramext.Slist1 $g$ >> - else if l > 5 & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in - List0ArgType t, <:expr< Gramext.Slist0 $g$ >> - else if l > 4 & String.sub s (l-4) 4 = "_opt" then - let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in - OptArgType t, <:expr< Gramext.Sopt $g$ >> - else - let t, se = - if tactic_genarg_level s <> None then - Some (ExtraArgType s), <:expr< Tactic. tactic >> - else - match Pcoq.entry_type (Pcoq.get_univ "prim") s with - | Some _ as x -> x, <:expr< Prim. $lid:s$ >> - | None -> - match Pcoq.entry_type (Pcoq.get_univ "constr") s with - | Some _ as x -> x, <:expr< Constr. $lid:s$ >> - | None -> - match Pcoq.entry_type (Pcoq.get_univ "tactic") s with - | Some _ as x -> x, <:expr< Tactic. $lid:s$ >> - | None -> None, <:expr< $lid:s$ >> in - let t = - match t with - | Some t -> t - | None -> -(* Pp.warning_with Pp_control.err_ft - ("Unknown primitive grammar entry: "^s);*) - ExtraArgType s - in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >> - open Pcaml EXTEND -- cgit v1.2.3