diff options
| -rw-r--r-- | lib/hMap.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 10 | ||||
| -rw-r--r-- | stm/stm.ml | 2 |
3 files changed, 6 insertions, 7 deletions
diff --git a/lib/hMap.ml b/lib/hMap.ml index 8e900cd58..b5fc52315 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -333,7 +333,6 @@ struct struct module IntM = Int.Map.Monad(M) module ExtM = Map.Monad(M) - open M let fold f s accu = let ff _ m accu = ExtM.fold f m accu in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5cfec1b0d..8808dbbac 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -496,10 +496,10 @@ module Bullet = struct | NoBulletInUse -> None | ProofFinished -> None | Suggest b -> Some ("Focus next goal with bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ Pp.string_of_ppcmds (pr_bullet b) ^".") | Unfinished b -> Some ("The current bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ Pp.string_of_ppcmds (pr_bullet b) ^ " is unfinished.") (* give always a message. *) @@ -508,9 +508,9 @@ module Bullet = struct | NeedClosingBrace -> "Try unfocusing with \"}\"." | NoBulletInUse -> assert false (* This should never raise an error. *) | ProofFinished -> "No more subgoals." - | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (pr_bullet b) ^ " is mandatory here.") - | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (pr_bullet b) ^ " is not finished.") exception FailedBullet of t * suggestion @@ -519,7 +519,7 @@ module Bullet = struct Errors.register_handler (function | FailedBullet (b,sugg) -> - let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in + let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (pr_bullet b) ^ " : " in Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) | _ -> raise Errors.Unhandled) diff --git a/stm/stm.ml b/stm/stm.ml index e0e787503..96f127aa2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1616,7 +1616,7 @@ end = struct (* {{{ *) let vernac_interp switch prev id q = assert(TaskQueue.n_workers (Option.get !queue) > 0); TaskQueue.enqueue_task (Option.get !queue) - QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch) + QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch) let init () = queue := Some (TaskQueue.create (if !Flags.async_proofs_full then 1 else 0)) |