diff options
| author | Vincent Laporte | 2019-05-06 14:05:09 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-10 16:06:10 +0000 |
| commit | 4e760a40f22e2d76a3d246b225d290eb5d15e9e8 (patch) | |
| tree | bc38af588c44ae04490a0d4febf17cec79323991 /pretyping/recordops.mli | |
| parent | 2f2658c5a318fb8a8c00caf4d1aca9fbc2d060d0 (diff) | |
[Canonical structures] Some projections may not be canonical
Diffstat (limited to 'pretyping/recordops.mli')
| -rw-r--r-- | pretyping/recordops.mli | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index f0594d513a..565454d3b3 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -17,14 +17,22 @@ open Constr (** A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) +type proj_kind = { + pk_name: Name.t; + pk_true_proj: bool; + pk_canonical: bool; +} + +val mk_proj_kind : Name.t -> bool -> proj_kind + type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; - s_PROJKIND : (Name.t * bool) list; + s_PROJKIND : proj_kind list; s_PROJ : Constant.t option list } type struc_tuple = - constructor * (Name.t * bool) list * Constant.t option list + constructor * proj_kind list * Constant.t option list val register_structure : Environ.env -> struc_tuple -> unit val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple |