diff options
| author | Emilio Jesus Gallego Arias | 2018-12-06 08:07:32 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-11 10:32:06 +0100 |
| commit | 913ccc7fb4a987ddd7c591d3c7d75579dc502a95 (patch) | |
| tree | 770f78f58393646c20e0ba007f3bb10ea4784dde /vernac/pvernac.ml | |
| parent | 97f5f37f782ffb9914fa8f67e745ba1effad20be (diff) | |
[api] Move reduction modules to `tactics`
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
Diffstat (limited to 'vernac/pvernac.ml')
| -rw-r--r-- | vernac/pvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index f26e0d0885..a647b2ef73 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,4 +52,4 @@ let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref let () = - register_grammar Stdarg.wit_red_expr (Vernac_.red_expr); + register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr); |