diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 26 |
1 files changed, 8 insertions, 18 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9b52d1bf31..b3233f8f08 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -115,7 +115,7 @@ GEXTEND Gram | Some (SelectNth g) -> c (Some g) | None -> c None | _ -> - VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) + VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) end ] ] ; located_vernac: @@ -260,7 +260,7 @@ GEXTEND Gram ProveBody (bl, t) ] ] ; reduce: - [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r + [ [ IDENT "Eval"; r = red_expr; "in" -> Some r | -> None ] ] ; one_decl_notation: @@ -580,12 +580,6 @@ 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 hint_info; @@ -663,10 +657,7 @@ GEXTEND Gram args = LIST0 argument_spec_block; more_implicits = OPT [ ","; impl = LIST1 - [ 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)] + [ impl = LIST0 more_implicits_block -> List.flatten impl] SEP "," -> impl ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> @@ -778,12 +769,11 @@ GEXTEND Gram ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)]) - | "/" -> (true (* Should warn about deprecated syntax *), []) + [ name = name -> [(snd name, Vernacexpr.NotImplicit)] | "["; items = LIST1 name; "]" -> - (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items) + List.map (fun name -> (snd name, Vernacexpr.Implicit)) items | "{"; items = LIST1 name; "}" -> - (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items) + List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items ] ]; strategy_level: @@ -924,7 +914,7 @@ GEXTEND Gram VernacRemoveOption ([table], v) ]] ; query_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> + [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) | IDENT "Compute"; c = lconstr -> fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) @@ -1081,7 +1071,7 @@ GEXTEND Gram (* registration of a custom reduction *) | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; - r = Tactic.red_expr -> + r = red_expr -> VernacDeclareReduction (s,r) ] ]; |