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 /engine/proofview.ml | |
| 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 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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 -> |