diff options
| author | Gaëtan Gilbert | 2019-11-22 15:56:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-26 14:11:32 +0100 |
| commit | 836cc0361cd3df76beeeb3178cc6f7d8e0fed388 (patch) | |
| tree | 1f6b08e508a91912ec08052d6ce6687fb90599ea /pretyping/coercion.mli | |
| parent | d7879b8566e48aabfdbee5c27bd4c29691352233 (diff) | |
coercion functions are never called without a term to coerce
(inh_conv_coerces_to is unused so we remove it)
This makes the code simpler, removing dead match branches and Option.maps/gets
Diffstat (limited to 'pretyping/coercion.mli')
| -rw-r--r-- | pretyping/coercion.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 3b24bcec8b..fe93a26f4f 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -54,13 +54,6 @@ val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> unsafe_judgment -> types -> evar_map * unsafe_judgment -(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] - is coercible to an object of type [t'] adding evar constraints if needed; - it fails if no coercion exists *) -val inh_conv_coerces_to : ?loc:Loc.t -> - env -> evar_map -> ?flags:Evarconv.unify_flags -> - types -> types -> evar_map - (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; raises [Not_found] if no coercion found *) |