slim down a bit genarg.ml (pr_intro_pattern forgotten there)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15380 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 1 insertions, 35 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index bbb4ae0a15..2daa1fe953 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,16 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Errors
-open Util
 open Names
-open Nameops
-open Nametab
 open Glob_term
 open Constrexpr
-open Term
-open Evd
 open Misctypes
 
 type argument_type =
@@ -54,8 +47,6 @@ type open_glob_constr = unit * glob_constr_and_expr
 
 type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern
 
-type 'a with_ebindings = 'a * open_constr bindings
-
 (* Dynamics but tagged by a type expression *)
 
 type 'a generic_argument = argument_type * Obj.t
@@ -64,25 +55,6 @@ type rlevel
 type glevel
 type tlevel
 
-let rec pr_intro_pattern (_,pat) = match pat with
-  | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
-  | IntroWildcard -> str "_"
-  | IntroRewrite true -> str "->"
-  | IntroRewrite false -> str "<-"
-  | IntroIdentifier id -> pr_id id
-  | IntroFresh id -> str "?" ++ pr_id id
-  | IntroForthcoming true -> str "*"
-  | IntroForthcoming false -> str "**"
-  | IntroAnonymous -> str "?"
-
-and pr_or_and_intro_pattern = function
-  | [pl] ->
-      str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
-  | pll ->
-      str "[" ++
-      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
-      ++ str "]"
-
 let rawwit_bool = BoolArgType
 let globwit_bool = BoolArgType
 let wit_bool = BoolArgType
@@ -240,7 +212,7 @@ type ('a,'b) abstract_argument_type = argument_type
 
 let create_arg v s =
   if List.mem_assoc s !dyntab then
-    anomaly ("Genarg.create: already declared generic argument " ^ s);
+    Errors.anomaly ("Genarg.create: already declared generic argument " ^ s);
   let t = ExtraArgType s in
   dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
   (t,t,t)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 7466ae46fd..3986d135ac 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Pp
 open Names
 open Term
@@ -31,11 +30,6 @@ type open_glob_constr = unit * glob_constr_and_expr
 
 type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
-type 'a with_ebindings = 'a * open_constr bindings
-
-val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds
-val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
-
 (** The route of a generic argument, from parsing to evaluation.
 In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.