diff options
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index bd468e62ad..1d381bb223 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -75,9 +75,19 @@ val inductive_class_of : inductive -> cl_index val class_args_of : env -> evar_map -> types -> constr list (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) -val declare_coercion : - coe_typ -> ?local:bool -> isid:bool -> - src:cl_typ -> target:cl_typ -> params:int -> unit +type coercion = { + coercion_type : coe_typ; + coercion_local : bool; + coercion_is_id : bool; + coercion_is_proj : Projection.Repr.t option; + coercion_source : cl_typ; + coercion_target : cl_typ; + coercion_params : int; +} + +val subst_coercion : substitution -> coercion -> coercion + +val declare_coercion : coercion -> unit (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool |