diff options
| author | Emilio Jesus Gallego Arias | 2018-12-06 04:44:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-09 02:54:02 +0100 |
| commit | d00472c59d15259b486868c5ccdb50b6e602a548 (patch) | |
| tree | 008d862e4308ac8ed94cfbcd94ac26c739b89642 /pretyping/typeclasses.mli | |
| parent | fa20a54d9fbe0f3872614a592fcef7ef56b05e49 (diff) | |
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index d00195678b..f8aedf88c2 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,33 +25,33 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen (** This module defines type-classes *) type typeclass = { + cl_univs : Univ.AUContext.t; (** The toplevel universe quantification in which the typeclass lives. In particular, [cl_props] and [cl_context] are quantified over it. *) - cl_univs : Univ.AUContext.t; + cl_impl : GlobRef.t; (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) - cl_impl : GlobRef.t; + cl_context : GlobRef.t option list * Constr.rel_context; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : GlobRef.t option list * Constr.rel_context; - (** Context of definitions and properties on defs, will not be shared *) cl_props : Constr.rel_context; + (** Context of definitions and properties on defs, will not be shared *) + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; - (** Whether we use matching or full unification during resolution *) cl_strict : bool; + (** Whether we use matching or full unification during resolution *) + cl_unique : bool; (** Whether we can assume that instances are unique, which allows no backtracking and sharing of resolution. *) - cl_unique : bool; } type instance |
