diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7cb897cf7..51c4733aa 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -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: @@ -867,7 +867,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) @@ -1024,7 +1024,7 @@ GEXTEND Gram (* registration of a custom reduction *) | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; - r = Tactic.red_expr -> + r = red_expr -> VernacDeclareReduction (s,r) ] ]; |