diff options
| author | Pierre-Marie Pédrot | 2016-04-11 14:10:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-12 20:49:12 +0200 |
| commit | 5ecdba3505a1dd8e713503657c1a0acbef0796a7 (patch) | |
| tree | d5f0d95ca9c0bdfb3cca01bf69393b352c5df6f7 | |
| parent | 116f8338b6fd60fdcf0f244772bcd6c82af5e333 (diff) | |
Warning for redundant TYPED AS clauses.
| -rw-r--r-- | grammar/argextend.ml4 | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 52119a963a..33cd62e3a9 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -76,7 +76,12 @@ let make_extend loc s cl wit = match cl with let declare_tactic_argument loc s (typ, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with | `Uniform (otyp, pr) -> - let typ = match otyp with Some typ -> typ | None -> ExtraArgType s in + let typ = match otyp with + | None -> ExtraArgType s + | Some typ -> + let () = if is_self s typ then Printf.eprintf "Redundant [TYPED AS %s] clause.\n%!" s in + typ + in typ, pr, typ, pr, otyp, pr | `Specialized (a, b, c, d, e, f) -> a, b, c, d, e, f in |