diff options
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 |