diff options
| author | Gaëtan Gilbert | 2018-06-23 15:38:00 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 13:49:17 +0200 |
| commit | 0108db19c96e1b46346f032964f2cca3f8149cb3 (patch) | |
| tree | 6414910c08328fceeb45c82414bea1ee0b601c91 /pretyping/classops.mli | |
| parent | 7817af48a554573fb649028263ecfc0fabe400d8 (diff) | |
Projections use index representation
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 35691ea37a..8df085e15c 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -21,7 +21,7 @@ type cl_typ = | CL_SECVAR of variable | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of Constant.t + | CL_PROJ of Projection.Repr.t (** Equality over [cl_typ] *) val cl_typ_eq : cl_typ -> cl_typ -> bool @@ -79,7 +79,7 @@ val declare_coercion : (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool -val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_universe_context_set +val coercion_value : coe_index -> (unsafe_judgment * bool * Projection.Repr.t option) Univ.in_universe_context_set (** {6 Lookup functions for coercion paths } *) |