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 :)
---
 engine/evd.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 0a8d1f3287..7560d68805 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -86,7 +86,7 @@ type evar_body =
 type evar_info = {
   evar_concl : econstr;
   (** Type of the evar. *)
-  evar_hyps : named_context_val; (** TODO econstr? *)
+  evar_hyps : named_context_val; (* TODO econstr? *)
   (** Context of the evar. *)
   evar_body : evar_body;
   (** Optional content of the evar. *)
@@ -546,6 +546,7 @@ val univ_flexible_alg : rigid
 type 'a in_evar_universe_context = 'a * UState.t
 
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
+
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
@@ -567,6 +568,7 @@ val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
 val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
     not a local sort variable declared in [evm] *)
+
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
 
 (* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *)
-- 
cgit v1.2.3