From 76f97eac9e0b6eee76469b2a00a9c157caa3da8a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:14:54 +0200 Subject: Remove more dead code (follow-up of previous commit). --- interp/constrextern.mli | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'interp/constrextern.mli') diff --git a/interp/constrextern.mli b/interp/constrextern.mli index ea627cff1..071898e16 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 -- cgit v1.2.3