From a3b4bde65a350bf3dc54ccec8f7608355c6a008a Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 18 Jun 2013 19:48:50 +0000
Subject: Proof-of-concept: moved four easy-to-handle generic arguments to
 their own file, Stdarg.

This required a little trick to correctly handle wit_* naming. We
use a dynamic table to remember exactly where those arguments come
from.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/printers.mllib  | 1 +
 dev/top_printers.ml | 4 ----
 2 files changed, 1 insertion(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 76fbbfdd51..c16b4abbac 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -125,6 +125,7 @@ Lexer
 Ppextend
 Pputils
 Genarg
+Stdarg
 Constrexpr_ops
 Notation_ops
 Topconstr
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4857b16cc1..939e9422ac 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -351,11 +351,7 @@ let pploc x = let (l,r) = Loc.unloc x in
 (* extendable tactic arguments *)
 let rec pr_argument_type = function
   (* Basic types *)
-  | BoolArgType -> str"bool"
-  | IntArgType -> str"int"
   | IntOrVarArgType -> str"int-or-var"
-  | StringArgType -> str"string"
-  | PreIdentArgType -> str"pre-ident"
   | IntroPatternArgType -> str"intro-pattern"
   | IdentArgType true -> str"ident"
   | IdentArgType false -> str"pattern_ident"
-- 
cgit v1.2.3