diff options
| author | Enrico Tassi | 2018-09-10 11:21:50 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-09-10 11:21:50 +0200 |
| commit | 2652465711423b0b332cfbb5f74145c48b53be1e (patch) | |
| tree | aea2a6163e5c8519c30f77fcfd781902285ff562 /pretyping/classops.mli | |
| parent | 69fb545f0fad2b356f5be1ce3e1a24b5afe26ce2 (diff) | |
| parent | 72da3cc8c5cf607c9c461491760837de2161123e (diff) | |
Merge PR #8104: Warnings on coercions used without being Imported
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index af00c0a8dc..dc193c4e74 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -113,3 +113,5 @@ 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 |