diff options
| -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 a4239713b6..07c1470c9e 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 16943d925d..eef16b1eb6 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 -> |