diff options
author | 2006-06-23 13:17:49 +0000 | |
---|---|---|
committer | 2006-06-23 13:17:49 +0000 | |
commit | 589217b0e6d5120975bc42fcb4fd7e6fb103b2c2 (patch) | |
tree | cf2116d3d075b74129031eab9b4a98f22720ef31 | |
parent | b603b1a781382e324925ae566d011e717071917c (diff) |
Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT EXTEND et TACTIC EXTEND
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8982 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | parsing/q_util.ml4 | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index eef16b1eb..ac1f3f050 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -84,24 +84,27 @@ let rec interp_entry_name loc s = OptArgType t, <:expr< Gramext.Sopt $g$ >> 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 + let t, se, lev = + match tactic_genarg_level s with + | Some n -> Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n + | None -> match Pcoq.entry_type (Pcoq.get_univ "prim") s with - | Some _ as x -> x, <:expr< Prim. $lid:s$ >> + | Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None | None -> match Pcoq.entry_type (Pcoq.get_univ "constr") s with - | Some _ as x -> x, <:expr< Constr. $lid:s$ >> + | Some _ as x -> x, <:expr< Constr. $lid:s$ >>, None | 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 + | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>, None + | None -> None, <:expr< $lid:s$ >>, None 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$) >> + | None -> ExtraArgType s in + let entry = match lev with + | Some n -> + let s = string_of_int n in + <:expr< Gramext.Snterml (Pcoq.Gram.Entry.obj $se$, $str:s$) >> + | None -> + <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >> + in t, entry |