mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

2 files changed, 36 insertions, 0 deletions

diff --git a/dev/include b/dev/include
index 563edd0420..42d2a01710 100644
--- a/dev/include
+++ b/dev/include
@@ -25,6 +25,7 @@
 #install_printer  (* tactic *) pptac;;
 #install_printer  (* object *) ppobj;;
 #install_printer  (* global_reference *) ppglobal;;
+#install_printer  (* generic_argument *) pp_generic_argument;;
 
 #install_printer  (* fconstr *) ppfconstr;;
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 276918706d..e1ee29e4f2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,6 +27,8 @@ open Clenv
 open Cerrors
 open Evd
 open Goptions
+open Genarg
+
 
 let _ = Constrextern.print_evar_arguments := true
 let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false
@@ -309,6 +311,39 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 let pploc x = let (l,r) = unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
 
+(* 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 -> str"ident"
+  | VarArgType -> str"var"
+  | RefArgType -> str"ref"
+  (* Specific types *)
+  | SortArgType -> str"sort"
+  | ConstrArgType -> str"constr"
+  | ConstrMayEvalArgType -> str"constr-may-eval"
+  | QuantHypArgType -> str"qhyp"
+  | OpenConstrArgType _ -> str"open-constr"
+  | ConstrWithBindingsArgType -> str"constr-with-bindings"
+  | BindingsArgType -> str"bindings"
+  | RedExprArgType -> str"redexp"
+  | List0ArgType t -> pr_argument_type t ++ str" list0"
+  | List1ArgType t -> pr_argument_type t ++ str" list1"
+  | OptArgType t -> pr_argument_type t ++ str" opt"
+  | PairArgType (t1,t2) ->
+      str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")"
+  | ExtraArgType s -> str"\"" ++ str s ++ str "\""
+
+let pp_argument_type t = pp (pr_argument_type t)
+
+let pp_generic_argument arg =
+  pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
+
 (**********************************************************************)
 (* Vernac-level debugging commands                                    *)