diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /stm | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.mli | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 4 |
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 |