diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 7616bfff6..7714cc810 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -49,7 +49,7 @@ let interp_prod_item lev = function | TacTerm s -> GramTerminal s | TacNonTerm (loc, nt, po) -> let sep = match po with Some (_,sep) -> sep | _ -> "" in - let (etyp, e) = interp_entry_name true (Some lev) nt sep in + let EntryName (etyp, e) = interp_entry_name true (TgTactic lev) nt sep in GramNonTerminal (loc, etyp, e, Option.map fst po) let make_terminal_status = function @@ -58,7 +58,7 @@ let make_terminal_status = function let rec make_tags = function | GramTerminal s :: l -> make_tags l - | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l + | GramNonTerminal (loc, etyp, _, po) :: l -> Genarg.unquote etyp :: make_tags l | [] -> [] let make_fresh_key = @@ -160,20 +160,22 @@ type atomic_entry = string * Genarg.glob_generic_argument list option type ml_tactic_grammar_obj = { mltacobj_name : Tacexpr.ml_tactic_name; (** ML-side unique name *) - mltacobj_prod : grammar_prod_item list list; + mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list; (** Grammar rules generating the ML tactic. *) } (** ML tactic notations whose use can be restricted to an identifier are added as true Ltac entries. *) let extend_atomic_tactic name entries = - let add_atomic (id, args) = match args with + let add_atomic i (id, args) = match args with | None -> () | Some args -> - let body = Tacexpr.TacML (Loc.ghost, name, args) in + let open Tacexpr in + let entry = { mltac_name = name; mltac_index = i } in + let body = TacML (Loc.ghost, entry, args) in Tacenv.register_ltac false false (Names.Id.of_string id) body in - List.iter add_atomic entries + List.iteri add_atomic entries let cache_ml_tactic_notation (_, obj) = extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod |