diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-27 14:58:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-27 15:39:10 +0200 |
| commit | b52dca14d3ac66ecd1657a21fecd0b48751096a7 (patch) | |
| tree | 193b1f22f433b24dd8038e54c2e96041acc6dd19 /toplevel | |
| parent | 0736cd1ff1eb07c6faae43cdfbe2efd11c8470e9 (diff) | |
Qualified ML tactic names. The plugin name is used to discriminate
potentially conflicting tactics names from different plugins.
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*) |