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/proofview.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 304b2dff84..8c15579bb0 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -660,9 +660,9 @@ let unifiable_delayed g l =
 let free_evars sigma l =
   let cache = Evarutil.create_undefined_evars_cache () in
   let map ev =
-  (** Computes the set of evars appearing in the hypotheses, the conclusion or
-      the body of the evar_info [evi]. Note: since we want to use it on goals,
-      the body is actually supposed to be empty. *)
+  (* Computes the set of evars appearing in the hypotheses, the conclusion or
+     the body of the evar_info [evi]. Note: since we want to use it on goals,
+     the body is actually supposed to be empty. *)
     let evi = Evd.find sigma ev in
     let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
     (ev, fevs)
@@ -672,9 +672,9 @@ let free_evars sigma l =
 let free_evars_with_state sigma l =
   let cache = Evarutil.create_undefined_evars_cache () in
   let map ev =
-  (** Computes the set of evars appearing in the hypotheses, the conclusion or
-      the body of the evar_info [evi]. Note: since we want to use it on goals,
-      the body is actually supposed to be empty. *)
+  (* Computes the set of evars appearing in the hypotheses, the conclusion or
+     the body of the evar_info [evi]. Note: since we want to use it on goals,
+     the body is actually supposed to be empty. *)
     let ev = drop_state ev in
     let evi = Evd.find sigma ev in
     let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
@@ -1157,7 +1157,7 @@ module Goal = struct
     let sigma = step.solution in
     let map goal =
       match cleared_alias sigma goal with
-      | None -> None (** ppedrot: Is this check really necessary? *)
+      | None -> None (* ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =
           Env.get >>= fun env ->
-- 
cgit v1.2.3