diff options
| author | Maxime Dénès | 2017-06-14 18:14:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 18:14:11 +0200 |
| commit | e70bec8fba8b15155aca41812225fcf42e1408e0 (patch) | |
| tree | 61839562df10cac70103a4250a45de278547b9c5 /interp | |
| parent | 42843f73e30eae57684269479193389242a0c1b1 (diff) | |
| parent | b36448114c3853311e31f533657a4d4e78b2820c (diff) | |
Merge PR#765: Remove obsolete Show commands
Diffstat (limited to 'interp')
| -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 f405100b1d..f0ee1d58a6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -181,9 +181,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 d771ee86fb..6c82168e48 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 |