diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-12 11:14:54 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-12 11:14:54 +0200 |
commit | 76f97eac9e0b6eee76469b2a00a9c157caa3da8a (patch) | |
tree | b6a076e12bae66fe62ef8b74b03a20989e3e23cb | |
parent | 2253d2eb4f892f932332358be8537fdb5552ef87 (diff) |
Remove more dead code (follow-up of previous commit).
-rw-r--r-- | interp/constrextern.ml | 3 | ||||
-rw-r--r-- | interp/constrextern.mli | 10 |
2 files changed, 0 insertions, 13 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d254520e0..668a2e6ac 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -74,9 +74,6 @@ let print_projections = ref false let print_meta_as_hole = ref false -let with_arguments f = Flags.with_option print_arguments f -let with_implicits f = Flags.with_option print_implicits f -let with_coercions f = Flags.with_option print_coercions f let with_universes f = Flags.with_option print_universes f let with_meta_as_hole f = Flags.with_option print_meta_as_hole f let without_symbols f = Flags.with_option print_no_symbol f 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 |