diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6f6bfc52e..fb1e0391b 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -128,7 +128,7 @@ let add_tactic_notation (local,n,prods,e) = type atomic_entry = string * Genarg.glob_generic_argument list option type ml_tactic_grammar_obj = { - mltacobj_name : string; + mltacobj_name : Tacexpr.ml_tactic_name; (** ML-side unique name *) mltacobj_prod : grammar_prod_item list list; (** Grammar rules generating the ML tactic. *) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 326af7bba..f48c4a700 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -23,7 +23,7 @@ val add_tactic_notation : type atomic_entry = string * Genarg.glob_generic_argument list option -val add_ml_tactic_notation : string -> +val add_ml_tactic_notation : ml_tactic_name -> Egramml.grammar_prod_item list list -> atomic_entry list -> unit (** Adding a (constr) notation in the environment*) |