diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-12 18:12:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-15 19:18:41 +0100 |
| commit | 9aa416c0c66ad7e14c4704898b74b99237d81c78 (patch) | |
| tree | 7b2519a4aa91a80c6c2c6e463389b13bbc5fa47e /pretyping/recordops.mli | |
| parent | 4fec6bdf0ad0f49c98a82538c5caf4511ba5e95c (diff) | |
Documenting check_record + changing a possibly undefined int into int option.
Diffstat (limited to 'pretyping/recordops.mli')
| -rw-r--r-- | pretyping/recordops.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 4a03d9bc5..054a3205a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -48,6 +48,7 @@ val find_projection : global_reference -> struc_typ the effective components of a structure and the projections of the structure *) +(** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = Const_cs of global_reference | Prod_cs @@ -57,13 +58,15 @@ type cs_pattern = type obj_typ = { o_DEF : constr; o_CTX : Univ.ContextSet.t; - o_INJ : int; (** position of trivial argument *) + o_INJ : int option; (** position of trivial argument *) o_TABS : constr list; (** ordered *) o_TPARAMS : constr list; (** ordered *) o_NPARAMS : int; o_TCOMPS : constr list } (** ordered *) -val cs_pattern_of_constr : constr -> cs_pattern * int * constr list +(** Return the form of the component of a canonical structure *) +val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list + val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ |