Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

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

1 files changed, 12 insertions, 2 deletions

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index cfa00c0068..614cbfdd42 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -19,6 +19,7 @@ open Nametab
 open Rawterm
 open Pattern
 open Topconstr
+open Symbols
 (*i*)
 
 (* Translation of pattern, cases pattern, rawterm and term into syntax
@@ -36,14 +37,23 @@ val extern_ref    : global_reference -> reference
 
 (* For debugging *)
 val print_implicits : bool ref
-val print_casts : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
 val print_universes : bool ref
 
-val with_casts : ('a -> 'b) -> 'a -> 'b
+(* This governs printing of implicit arguments. If [with_implicits] is
+   on and not [with_arguments] then implicit args are printed prefixed
+   by "!"; if [with_implicits] and [with_arguments] are both on the
+   function and not the arguments is prefixed by "!" *)
 val with_implicits : ('a -> 'b) -> 'a -> 'b
 val with_arguments : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing of coercions *)
 val with_coercions : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing universe names of Type{.} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
+
+(* This suppresses printing of numeral and symbols *)
+val without_symbols : ('a -> 'b) -> 'a -> 'b