From 89b38ee15e02349c8d4b05df3170e3c97d8d1bf9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:04 +0200
Subject: Revert "Fixing printers for pr_auto_using and pr_firstorder_using."

This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
---
 ltac/g_auto.ml4 | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'ltac')

diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 601d39b995..d4fd8a1df3 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -50,16 +50,11 @@ let eval_uconstrs ist cs =
   } in
   List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
 
-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
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
 
 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
@@ -197,6 +192,8 @@ ARGUMENT EXTEND 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