From d00472c59d15259b486868c5ccdb50b6e602a548 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Dec 2018 04:44:27 +0100
Subject: [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 :)
---
 pretyping/typeclasses.mli | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'pretyping/typeclasses.mli')

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
-- 
cgit v1.2.3