diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/library.ml | 10 | ||||
| -rw-r--r-- | vernac/library.mli | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
3 files changed, 9 insertions, 9 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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index af40292f18..54f034c74e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -413,7 +413,7 @@ let sort_universes g = let levels = traverse LMap.empty [normalize Level.set, 0] in let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in + let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in let ulevels = Array.cons Level.set ulevels in (* Add the normal universes *) let fold (cur, ans) u = |