diff options
| -rw-r--r-- | grammar/tacextend.mlp | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 |
2 files changed, 15 insertions, 5 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 175853d50..fe864ed40 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -48,7 +48,7 @@ let make_fun_clauses loc s l = let map c = GramCompat.make_fun loc [make_clause c] in mlexpr_of_list map l -let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >> +let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> let rec mlexpr_of_symbol = function | Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7bc5bfca3..71d16d682 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: |