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/library.mli | |
| parent | 004bf5770bdcdd1b35dd27f683c733505823e741 (diff) | |
Remove remote counter system
Diffstat (limited to 'vernac/library.mli')
| -rw-r--r-- | vernac/library.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |