diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f0d90b11b8..2eec7848ae 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -807,6 +807,12 @@ GEXTEND Gram | IDENT "Debug"; IDENT "Off" -> VernacSetOption (None,["Ltac";"Debug"], BoolValue false) +(* registration of a custom reduction *) + + | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; + r = Tactic.red_expr -> + VernacDeclareReduction (use_locality(),s,r) + ] ]; END ;; |