aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.mli')
-rw-r--r--interp/constrextern.mli10
1 files changed, 0 insertions, 10 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index d771ee86f..6c82168e4 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -59,16 +59,6 @@ val set_extern_reference :
val get_extern_reference :
unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
-(** 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