diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-11 18:18:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-11 19:38:24 +0200 |
| commit | 2a2d418971a019202cdb78fabc7658a543f0886d (patch) | |
| tree | 0292c97712ab9ac39b1595a498aec131cbc1227f | |
| parent | 7bc1610376fac29397be39d4a06b178e8e35e66e (diff) | |
Adding a test to check whether two tactic notations conflict.
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 3 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 7 |
3 files changed, 12 insertions, 0 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index ffff44d5b..08e8bc011 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -26,6 +26,8 @@ let interp_alias key = try KNmap.find key !alias_map with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) +let check_alias key = KNmap.mem key !alias_map + (** ML tactic extensions (TacML) *) type ml_tactic = diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4c..9410ccb38 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -23,6 +23,9 @@ val register_alias : alias -> glob_tactic_expr -> unit val interp_alias : alias -> glob_tactic_expr (** Recover the the body of an alias. Raises an anomaly if it does not exist. *) +val check_alias : alias -> bool +(** Returns [true] if an alias is defined, false otherwise. *) + (** {5 Coq tactic definitions} *) val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index f4fabc4d3..300bf5b49 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -84,8 +84,14 @@ type tactic_grammar_obj = { tacobj_body : Tacexpr.glob_tactic_expr } +let check_key key = + if Tacenv.check_alias key then + error "Conflicting tactic notations keys. This can happen when including \ + twice the same module." + let cache_tactic_notation (_, tobj) = let key = tobj.tacobj_key in + let () = check_key key in Tacenv.register_alias key tobj.tacobj_body; Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp @@ -97,6 +103,7 @@ let open_tactic_notation i (_, tobj) = let load_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in + let () = check_key key in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; |