diff options
| author | Maxime Dénès | 2018-07-18 18:22:24 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-25 13:07:36 +0000 |
| commit | d12cc91d07bc473276316474cc8f8beb9040934c (patch) | |
| tree | 0dd3b9c46cbb330813ebf34701100d39ba4ac74e /pretyping/classops.mli | |
| parent | fd065eae52dde32bcb95955f6da9280fed780729 (diff) | |
Remove `Automatic Coercions Import` option.
This option made the Coercions command follow non-standard scoping rules
(effect on `Require` rather than `Import`). It was already marked for deletion
in 8.8.
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 7c4842c8ae..ed2c5478f0 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -113,5 +113,3 @@ val coercions : unit -> coe_info_typ list (** [hide_coercion] returns the number of params to skip if the coercion must be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) val hide_coercion : coe_typ -> int option - -val is_coercion_in_scope : GlobRef.t -> bool |