diff options
| author | Gaëtan Gilbert | 2021-03-26 15:34:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-04-14 12:54:38 +0200 |
| commit | 3efee577b4c92b38a987b40e555fae2c0a2023c4 (patch) | |
| tree | 182f9cd42fdb9969bab3149f3add552c7455de2e /vernac | |
| parent | 004bf5770bdcdd1b35dd27f683c733505823e741 (diff) | |
Remove remote counter system
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/library.ml | 10 | ||||
| -rw-r--r-- | vernac/library.mli | 6 |
2 files changed, 8 insertions, 8 deletions
diff --git a/vernac/library.ml b/vernac/library.ml index cc9e3c3c44..eedf8aa670 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -448,10 +448,10 @@ let save_library_base f sum lib univs tasks proofs = Sys.remove f; Exninfo.iraise reraise -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) let save_library_to todo_proofs ~output_native_objects dir f otab = assert( @@ -464,7 +464,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let except = match todo_proofs with | ProofsTodoNone -> Future.UUIDSet.empty | ProofsTodoSomeEmpty except -> except - | ProofsTodoSome (except,l,_) -> except + | ProofsTodoSome (except,l) -> except in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, f2t_map = Opaqueproof.dump ~except otab in @@ -473,13 +473,13 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = | ProofsTodoNone -> None, None | ProofsTodoSomeEmpty _except -> None, Some (Univ.ContextSet.empty,false) - | ProofsTodoSome (_except, tasks, rcbackup) -> + | ProofsTodoSome (_except, tasks) -> let tasks = List.map Stateid.(fun (r,b) -> try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b with Not_found -> assert b; { r with uuid = -1 }, b) tasks in - Some (tasks,rcbackup), + Some tasks, Some (Univ.ContextSet.empty,false) in let sd = { diff --git a/vernac/library.mli b/vernac/library.mli index d0e9f84691..4c6c654c58 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -41,13 +41,13 @@ type seg_proofs = Opaqueproof.opaque_proofterm array argument. [output_native_objects]: when producing vo objects, also compile the native-code version. *) -type ('document,'counters) todo_proofs = +type 'document todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list (* for .vio *) val save_library_to : - ('document,'counters) todo_proofs -> + 'document todo_proofs -> output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit |