aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/coqworkmgrApi.ml4
-rw-r--r--stm/dag.mli6
-rw-r--r--stm/proofBlockDelimiter.ml6
-rw-r--r--stm/vcs.ml14
-rw-r--r--stm/vcs.mli18
-rw-r--r--stm/vernac_classifier.ml6
-rw-r--r--stm/vio_checking.ml6
-rw-r--r--stm/workerPool.ml2
-rw-r--r--stm/workerPool.mli2
9 files changed, 32 insertions, 32 deletions
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 92dc77172f..2b39a7a2aa 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -69,7 +69,7 @@ let parse_response s =
let p = try int_of_string p with _ -> raise ParseError in
Pong (n,m,p)
| _ -> raise ParseError
-
+
let print_request = function
| Hello Low -> "HELLO LOW\n"
| Hello High -> "HELLO HIGH\n"
@@ -101,7 +101,7 @@ let option_map f = function None -> None | Some x -> Some (f x)
let init p =
try
let sock = Sys.getenv "COQWORKMGR_SOCK" in
- manager := option_map (fun s ->
+ manager := option_map (fun s ->
let cout = Unix.out_channel_of_descr s in
set_binary_mode_out cout true;
let cin = Unix.in_channel_of_descr s in
diff --git a/stm/dag.mli b/stm/dag.mli
index 3a291c8d52..1cd593fdad 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -9,12 +9,12 @@
(************************************************************************)
module type S = sig
-
+
type node
module NodeSet : Set.S with type elt = node
type ('edge,'info,'cdata) t
-
+
val empty : ('e,'i,'d) t
val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t
@@ -45,7 +45,7 @@ module type S = sig
val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
- val iter : ('e,'i,'d) t ->
+ val iter : ('e,'i,'d) t ->
(node -> 'd Property.t list -> 'i option ->
(node * 'e) list -> unit) -> unit
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index a487799b74..0e8c463b19 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -108,7 +108,7 @@ let () = register_proof_block_delimiter
"bullet" static_bullet dynamic_bullet
(* ******************** { block } ***************************************** *)
-
+
let static_curly_brace ({ entry_point; prev_node } as view) =
let open Vernacexpr in
assert(entry_point.ast.CAst.v.expr = VernacEndSubproof);
@@ -169,7 +169,7 @@ let static_indent ({ entry_point; prev_node } as view) =
else
crawl view ~init:(Some last_tac) (fun prev node ->
if node.indentation >= last_tac.indentation then `Cont node
- else
+ else
`Found { block_stop = entry_point.id; block_start = node.id;
dynamic_switch = node.id;
carry_on_data = of_vernac_control_val entry_point.ast }
@@ -180,7 +180,7 @@ let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
match is_focused_goal_simple ~doc id with
| `Simple [] -> `Leaks
| `Simple focused ->
- let but_last = List.tl (List.rev focused) in
+ let but_last = List.tl (List.rev focused) in
`ValidBlock {
base_state = id;
goals_to_admit = but_last;
diff --git a/stm/vcs.ml b/stm/vcs.ml
index 78edeb53d3..26be9ae76f 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -24,20 +24,20 @@ module type S = sig
end
type id
-
+
type ('kind) branch_info = {
kind : [> `Master] as 'kind;
root : id;
pos : id;
}
-
+
type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ]
-
+
val empty : id -> ('kind,'diff,'info,'property_data) t
-
+
val current_branch : ('k,'e,'i,'c) t -> Branch.t
val branches : ('k,'e,'i,'c) t -> Branch.t list
-
+
val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t
val branch :
@@ -52,7 +52,7 @@ module type S = sig
('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
Branch.t -> ('k,'diff,'i,'c) t
val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
-
+
val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
val get_info : ('k,'e,'info,'c) t -> id -> 'info option
@@ -62,7 +62,7 @@ module type S = sig
val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
- val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
+ val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
(* Removes all unreachable nodes and returns them *)
val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
diff --git a/stm/vcs.mli b/stm/vcs.mli
index f6ca81257b..584560f833 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -41,20 +41,20 @@ module type S = sig
end
type id
-
+
type ('kind) branch_info = {
kind : [> `Master] as 'kind;
root : id;
pos : id;
}
-
+
type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ]
-
+
val empty : id -> ('kind,'diff,'info,'property_data) t
-
+
val current_branch : ('k,'e,'i,'c) t -> Branch.t
val branches : ('k,'e,'i,'c) t -> Branch.t list
-
+
val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t
val branch :
@@ -69,25 +69,25 @@ module type S = sig
('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
Branch.t -> ('k,'diff,'i,'c) t
val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
-
+
val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
val get_info : ('k,'e,'info,'c) t -> id -> 'info option
(* Read only dag *)
module Dag : Dag.S with type node = id
val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t
-
+
(* Properties are not a concept typical of a VCS, but a useful metadata
* of a DAG (or graph). *)
val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
- val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
+ val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
(* Removes all unreachable nodes and returns them *)
val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t
-
+
end
module Make(OT : Map.OrderedType) : S
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index ff0bf0ac2a..c5b3e0931b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -74,7 +74,7 @@ let classify_vernac e =
| VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
| VernacCheckMayEval _ -> VtQuery
(* ProofStep *)
- | VernacProof _
+ | VernacProof _
| VernacFocus _ | VernacUnfocus
| VernacSubproof _
| VernacCheckGuard
@@ -83,7 +83,7 @@ let classify_vernac e =
VtProofStep { parallel = `No; proof_block_detection = None }
| VernacBullet _ ->
VtProofStep { parallel = `No; proof_block_detection = Some "bullet" }
- | VernacEndSubproof ->
+ | VernacEndSubproof ->
VtProofStep { parallel = `No;
proof_block_detection = Some "curly" }
(* StartProof *)
@@ -146,7 +146,7 @@ let classify_vernac e =
| VernacUniverse _ | VernacConstraint _
| VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
| VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
- | VernacChdir _
+ | VernacChdir _
| VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
| VernacArguments _
| VernacReserve _
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index baa7b3570c..837ba3d880 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -52,7 +52,7 @@ let schedule_vio_checking j fs =
| ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl
| ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in
aux f [] l in
- let prog = Sys.argv.(0) in
+ let prog = Sys.argv.(0) in
let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
let make_job () =
let cur = ref 0.0 in
@@ -79,7 +79,7 @@ let schedule_vio_checking j fs =
let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
List.flatten
(List.map (fun (f, tl) ->
- "-check-vio-tasks" ::
+ "-check-vio-tasks" ::
String.concat "," (List.map string_of_int tl) :: [f])
(pack (List.sort cmp_job !what))) in
let rc = ref 0 in
@@ -115,7 +115,7 @@ let schedule_vio_compilation j fs =
| s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest)
| _ :: rest when b -> filter_argv b rest
| s :: rest -> s :: filter_argv b rest in
- let prog = Sys.argv.(0) in
+ let prog = Sys.argv.(0) in
let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
let all_jobs = !jobs in
let make_job () =
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index f77ced2f3a..d82741576e 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -88,7 +88,7 @@ let rec create_worker extra pool priority id =
let cpanel = { exit; cancelled; extra } in
let manager = CThread.create (Model.manager cpanel) worker in
{ name; cancel; manager; process }
-
+
and cleanup x priority = locking x begin fun { workers; count; extra_arg } ->
workers := List.map (function
| { cancel } as w when !cancel = false -> w
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index 5468a24959..88175a788c 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -31,7 +31,7 @@ end
module Make(Model : PoolModel) : sig
type pool
-
+
val create : Model.extra -> size:int -> CoqworkmgrApi.priority -> pool
val is_empty : pool -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:38:48 +0000