From a4db30e1cd6c21a466549835a86d61f95db36c82 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Apr 2016 22:24:59 +0200
Subject: Fixing printers for pr_auto_using and pr_firstorder_using.

---
 ltac/g_auto.ml4 | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'ltac')

diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index c561ecf606..6a8fa8d698 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -50,11 +50,17 @@ let eval_uconstrs ist cs =
   } in
   List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
 
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
+let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
+let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob
 
 ARGUMENT EXTEND auto_using
   TYPED AS uconstr_list
   PRINTED BY pr_auto_using
+  RAW_TYPED AS uconstr_list
+  RAW_PRINTED BY pr_auto_using_raw
+  GLOB_TYPED AS uconstr_list
+  GLOB_PRINTED BY pr_auto_using_glob
 | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ]
 | [ ] -> [ [] ]
 END
@@ -206,8 +212,6 @@ GLOB_PRINTED BY pr_hints_path
 | [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ]
 END
 
-let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
-
 ARGUMENT EXTEND opthints
   TYPED AS preident_list_opt
   PRINTED BY pr_hintbases
-- 
cgit v1.2.3