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 /plugins/firstorder | |
| 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 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 37fc81ee38..ea86a4b514 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -132,7 +132,7 @@ let normalize_evaluables= open Ppconstr open Printer let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid -let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) +let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global let warn_deprecated_syntax = |