Options d'affichage maintenant dans Constrextern

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

2 files changed, 9 insertions, 3 deletions

diff --git a/parsing/termast.ml b/parsing/termast.ml
index f1ce602fb..8405c6cf1 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -31,24 +31,29 @@ open Nametab
 
 (**********************************************************************)
 (* Parametrization                                                    *)
-
+open Constrextern
+(*
 (* This governs printing of local context of references *)
 let print_arguments = ref false
 
 (* If true, prints local context of evars, whatever print_arguments *)
 let print_evar_arguments = ref false
+*)
 
 (* This forces printing of cast nodes *)
 let print_casts = ref true
 
+(*
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
    how implicit args are printed. If on, implicit args are printed
    prefixed by "!" otherwise the function and not the arguments is
    prefixed by "!" *)
 let print_implicits = ref false
+*)
 let print_implicits_explicit_args = ref false
 
+(*
 (* This forces printing of coercions *)
 let print_coercions = ref false
 
@@ -66,7 +71,7 @@ let with_casts f = with_option print_casts f
 let with_implicits f = with_option print_implicits f
 let with_coercions f = with_option print_coercions f
 let with_universes f = with_option print_universes f
-
+*)
 (**********************************************************************)
 (* conversion of references                                           *)
 
diff --git a/parsing/termast.mli b/parsing/termast.mli
index c6e94fe16..9b87af5f8 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -39,7 +39,7 @@ val ast_of_inductive    : env -> inductive -> Coqast.t
 val ast_of_ref          : global_reference -> Coqast.t
 val ast_of_qualid       : qualid -> Coqast.t
 
-(* For debugging *)
+(*i Now in constrextern.mli
 val print_implicits : bool ref
 val print_casts : bool ref
 val print_arguments : bool ref
@@ -52,3 +52,4 @@ val with_implicits : ('a -> 'b) -> 'a -> 'b
 val with_arguments : ('a -> 'b) -> 'a -> 'b
 val with_coercions : ('a -> 'b) -> 'a -> 'b
 val with_universes : ('a -> 'b) -> 'a -> 'b
+i*)