diff options
| author | Maxime Dénès | 2016-11-03 09:45:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-03 09:45:09 +0100 |
| commit | c40331793c6397e6a4185d98a67543c4c1e2cb23 (patch) | |
| tree | 547c042c71a5f708a7c890a3070271b2f77074fe /parsing | |
| parent | 9c52d25ac0badc5ec6eb0eb897219e607c362e83 (diff) | |
| parent | df1720bff67889818f8b4856f29ac02540d7f756 (diff) | |
Merge branch 'v8.6' into trunk
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7bc5bfca38..71d16d682a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -580,6 +580,12 @@ let warn_deprecated_implicit_arguments = CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") +let warn_deprecated_arguments_syntax = + CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated" + (fun () -> strbrk "The \"/\" modifier has an effect only in the first " + ++ strbrk "arguments list. The syntax allowing it to appear" + ++ strbrk " in other lists is deprecated.") + (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name; @@ -654,7 +660,10 @@ GEXTEND Gram args = LIST0 argument_spec_block; more_implicits = OPT [ ","; impl = LIST1 - [ impl = LIST0 more_implicits_block -> List.flatten impl] + [ impl = LIST0 more_implicits_block -> + let warn_slash = List.exists fst impl in + if warn_slash then warn_deprecated_arguments_syntax ~loc:!@loc (); + List.flatten (List.map snd impl)] SEP "," -> impl ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> @@ -766,11 +775,12 @@ GEXTEND Gram ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> [(snd name, Vernacexpr.NotImplicit)] + [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)]) + | "/" -> (true (* Should warn about deprecated syntax *), []) | "["; items = LIST1 name; "]" -> - List.map (fun name -> (snd name, Vernacexpr.Implicit)) items + (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items) | "{"; items = LIST1 name; "}" -> - List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items + (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items) ] ]; strategy_level: |