diff options
| author | Maxime Dénès | 2019-04-04 22:08:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | dd672f839765c656a910ff8e07603858dbc8bc38 (patch) | |
| tree | 5266f2fe3b129cfe887e7174c4ec5901e5e3f8b1 /pretyping/classops.mli | |
| parent | bf5f0520cf105afb048c6eac5d6de1d3e1a719df (diff) | |
Move vernac-related part of coercions to vernac
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 |