aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-12-06 04:44:27 +0100
committerEmilio Jesus Gallego Arias2018-12-09 02:54:02 +0100
commitd00472c59d15259b486868c5ccdb50b6e602a548 (patch)
tree008d862e4308ac8ed94cfbcd94ac26c739b89642 /pretyping/typeclasses.mli
parentfa20a54d9fbe0f3872614a592fcef7ef56b05e49 (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.mli14
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