diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.mli | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 11 |
3 files changed, 7 insertions, 7 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 94e04d1842..51166cf238 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,7 +60,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of UnivGen.universe_id list + | MoreDataUnivLevel of UnivGen.univ_unique_id list let slave_respond (Request r) = let res = T.perform r in 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 94405924b7..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) @@ -1543,7 +1543,7 @@ end = struct (* {{{ *) let pobject, _ = Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) - Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in + Lemmas.(standard_proof_terminator []) in let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop @@ -1682,9 +1682,8 @@ end = struct (* {{{ *) `OK_ADMITTED else begin (* The original terminator, a hook, has not been saved in the .vio*) - Proof_global.set_terminator - (Lemmas.standard_proof_terminator [] - (Lemmas.mk_hook (fun _ _ -> ()))); + Proof_global.set_terminator (Lemmas.standard_proof_terminator []); + let opaque = Proof_global.Opaque in let proof = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in @@ -1751,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 |