diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-23 10:03:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-23 10:03:54 +0000 |
| commit | 93642cdc3acb9f4e8d1b4ac1f1621d1104f04e54 (patch) | |
| tree | 5f3be6d99c001bb3219b3d5e2972f7e37790534f /parsing | |
| parent | 3f024bf1ae2b84028a631a8361c960022b9fe803 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/argextend.ml4 | 35 | ||||
| -rw-r--r-- | parsing/q_util.ml4 | 3 |
2 files changed, 3 insertions, 35 deletions
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 diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 16943d925..eef16b1eb 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -85,6 +85,9 @@ let rec interp_entry_name loc s = else let s = if s = "hyp" then "var" else s in 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 -> |