aboutsummaryrefslogtreecommitdiff
path: root/stm
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 /stm
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 'stm')
-rw-r--r--stm/asyncTaskQueue.mli1
-rw-r--r--stm/stm.ml4
2 files changed, 3 insertions, 2 deletions
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index 6e6827c73f..067ea5df0c 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -70,6 +70,7 @@ module type Task = sig
(** UID of the task kind, for -toploop *)
val name : string ref
+
(** Extra arguments of the task kind, for -toploop *)
val extra_env : unit -> string array
diff --git a/stm/stm.ml b/stm/stm.ml
index 3444229735..e835bdcb1e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1087,7 +1087,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
(stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
else
match cmd with
- | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *)
+ | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *)
| _ ->
stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr)
@@ -1750,7 +1750,7 @@ end = struct (* {{{ *)
let uc =
Option.get
(Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
- (** We only manipulate monomorphic terms here. *)
+ (* We only manipulate monomorphic terms here. *)
let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
let pr =
Future.from_val (map (Option.get (Global.body_of_constant_body c))) in