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 | |
| 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')
| -rw-r--r-- | vernac/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e7c1e29beb..46854b7f5d 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -700,7 +700,7 @@ open Pputils | None -> mt() | Some r -> keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ + Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -1134,7 +1134,7 @@ open Pputils let pr_mayeval r c = match r with | Some r0 -> hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in @@ -1146,7 +1146,7 @@ open Pputils | VernacDeclareReduction (s,r) -> return ( keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r ) | VernacPrint p -> return (pr_printable p) 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); |