diff options
Diffstat (limited to 'interp/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 14 |
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 |