aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/geninterp.ml4
-rw-r--r--interp/genintern.ml2
-rw-r--r--lib/cSig.mli2
-rw-r--r--lib/dyn.ml2
-rw-r--r--lib/dyn.mli3
-rw-r--r--lib/exninfo.ml2
-rw-r--r--lib/genarg.ml2
-rw-r--r--lib/spawn.ml4
-rw-r--r--lib/spawn.mli4
-rw-r--r--lib/store.ml6
-rw-r--r--lib/store.mli7
-rw-r--r--library/libobject.ml2
-rw-r--r--library/summary.ml2
-rw-r--r--parsing/pcoq.ml4
-rw-r--r--stm/asyncTaskQueue.ml8
-rw-r--r--stm/asyncTaskQueue.mli4
-rw-r--r--stm/proofworkertop.ml2
-rw-r--r--stm/queryworkertop.ml2
-rw-r--r--stm/stm.ml8
-rw-r--r--stm/tacworkertop.ml2
-rw-r--r--stm/vio_checking.ml2
-rw-r--r--tools/fake_ide.ml2
23 files changed, 31 insertions, 48 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 324f883e8..a668826a7 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -124,8 +124,7 @@ end
(* The type of mappings for existential variables *)
-module Dummy = struct end
-module Store = Store.Make(Dummy)
+module Store = Store.Make ()
type evar = Term.existential_key
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index e79e258fb..6c629468b 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -9,11 +9,11 @@
open Names
open Genarg
-module TacStore = Store.Make(struct end)
+module TacStore = Store.Make ()
(** Dynamic toplevel values *)
-module ValT = Dyn.Make(struct end)
+module ValT = Dyn.Make ()
module Val =
struct
diff --git a/interp/genintern.ml b/interp/genintern.ml
index f4996c997..2f2edab30 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -10,7 +10,7 @@ open Names
open Mod_subst
open Genarg
-module Store = Store.Make(struct end)
+module Store = Store.Make ()
type glob_sign = {
ltacvars : Id.Set.t;
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 151cfbdca..6910cbbf0 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -48,8 +48,6 @@ end
(** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml
documentation for more information. *)
-module type EmptyS = sig end
-
module type MapS =
sig
type key
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 6bd43455f..1544f1246 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -59,7 +59,7 @@ sig
end
-module Make(M : CSig.EmptyS) = struct
+module Make () = struct
module Self : PreS = struct
(* Dynamics, programmed with DANGER !!! *)
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e43c8a9bc..d3483cd5f 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -59,5 +59,4 @@ end
end
-(** FIXME: use OCaml 4.02 generative functors when available *)
-module Make(M : CSig.EmptyS) : S
+module Make () : S
diff --git a/lib/exninfo.ml b/lib/exninfo.ml
index d049dc6cf..167d3d6dc 100644
--- a/lib/exninfo.ml
+++ b/lib/exninfo.ml
@@ -10,7 +10,7 @@
containing a pair composed of the distinguishing [token] and the backtrace
information. We discriminate the token by pointer equality. *)
-module Store = Store.Make(struct end)
+module Store = Store.Make ()
type 'a t = 'a Store.field
diff --git a/lib/genarg.ml b/lib/genarg.ml
index b78fe4037..a3bfb405c 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -11,7 +11,7 @@ open Util
module ArgT =
struct
- module DYN = Dyn.Make(struct end)
+ module DYN = Dyn.Make ()
module Map = DYN.Map
type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag
type any = Any : ('a, 'b, 'c) tag -> any
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 0cf163e73..de31d87d0 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -28,8 +28,6 @@ module type Control = sig
end
-module type Empty = sig end
-
module type MainLoopModel = sig
type async_chan
type condition
@@ -216,7 +214,7 @@ let rec wait p =
end
-module Sync(T : Empty) = struct
+module Sync () = struct
type process = {
cin : in_channel;
diff --git a/lib/spawn.mli b/lib/spawn.mli
index a131715e9..fd2b92ae3 100644
--- a/lib/spawn.mli
+++ b/lib/spawn.mli
@@ -34,8 +34,6 @@ module type Control = sig
end
(* Abstraction to work with both threads and main loop models *)
-module type Empty = sig end
-
module type MainLoopModel = sig
type async_chan
type condition
@@ -64,7 +62,7 @@ module Async(ML : MainLoopModel) : sig
end
(* spawn a process and read its output synchronously *)
-module Sync(T : Empty) : sig
+module Sync () : sig
type process
val spawn :
diff --git a/lib/store.ml b/lib/store.ml
index a1788f7da..97a8fea08 100644
--- a/lib/store.ml
+++ b/lib/store.ml
@@ -14,10 +14,6 @@
stores, we might want something static to avoid troubles with
plugins order. *)
-module type T =
-sig
-end
-
module type S =
sig
type t
@@ -30,7 +26,7 @@ sig
val field : unit -> 'a field
end
-module Make (M : T) : S =
+module Make () : S =
struct
let next =
diff --git a/lib/store.mli b/lib/store.mli
index 8eab314ed..5cc5bb859 100644
--- a/lib/store.mli
+++ b/lib/store.mli
@@ -9,11 +9,6 @@
(*** This module implements an "untyped store", in this particular case we
see it as an extensible record whose fields are left unspecified. ***)
-module type T =
-sig
-(** FIXME: Waiting for first-class modules... *)
-end
-
module type S =
sig
type t
@@ -42,5 +37,5 @@ sig
end
-module Make (M : T) : S
+module Make () : S
(** Create a new store type. *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 013c6fa0a..0c11be9ab 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -9,7 +9,7 @@
open Libnames
open Pp
-module Dyn = Dyn.Make(struct end)
+module Dyn = Dyn.Make ()
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
diff --git a/library/summary.ml b/library/summary.ml
index 69eff830d..9f49d1f83 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -10,7 +10,7 @@ open Pp
open CErrors
open Util
-module Dyn = Dyn.Make(struct end)
+module Dyn = Dyn.Make ()
type marshallable = [ `Yes | `No | `Shallow ]
type 'a summary_declaration = {
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 3d00b220b..d34da159e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -543,11 +543,11 @@ let epsilon_value f e =
(** Synchronized grammar extensions *)
-module GramState = Store.Make(struct end)
+module GramState = Store.Make ()
type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
-module GrammarCommand = Dyn.Make(struct end)
+module GrammarCommand = Dyn.Make ()
module GrammarInterp = struct type 'a t = 'a grammar_extension end
module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 5d9b595d3..a356f32e9 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -49,7 +49,7 @@ end
type expiration = bool ref
-module Make(T : Task) = struct
+module Make(T : Task) () = struct
exception Die
type response =
@@ -107,7 +107,7 @@ module Make(T : Task) = struct
let open Feedback in
feedback ~id:Stateid.initial (WorkerStatus(id, s))
- module Worker = Spawn.Sync(struct end)
+ module Worker = Spawn.Sync ()
module Model = struct
@@ -354,5 +354,5 @@ module Make(T : Task) = struct
end
-module MakeQueue(T : Task) = struct include Make(T) end
-module MakeWorker(T : Task) = struct include Make(T) end
+module MakeQueue(T : Task) () = struct include Make(T) () end
+module MakeWorker(T : Task) () = struct include Make(T) () end
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index a80918e93..1044e668b 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -41,7 +41,7 @@ end
type expiration = bool ref
-module MakeQueue(T : Task) : sig
+module MakeQueue(T : Task) () : sig
type queue
@@ -76,7 +76,7 @@ module MakeQueue(T : Task) : sig
end
-module MakeWorker(T : Task) : sig
+module MakeWorker(T : Task) () : sig
val main_loop : unit -> unit
val init_stdout : unit -> unit
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index a27c6d6cd..10b42f7e9 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index ac7a270ac..a1fe50c63 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
diff --git a/stm/stm.ml b/stm/stm.ml
index 84a4c5cc5..3cac3b609 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -179,7 +179,7 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
let default_info () =
{ n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
-module DynBlockData : Dyn.S = Dyn.Make(struct end)
+module DynBlockData : Dyn.S = Dyn.Make ()
(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose
* no constraint on properties, here we impose boxes to be non overlapping.
@@ -1558,7 +1558,7 @@ and Slaves : sig
end = struct (* {{{ *)
- module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask)
+ module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) ()
let queue = ref None
let init () =
@@ -1884,7 +1884,7 @@ and Partac : sig
end = struct (* {{{ *)
- module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
+ module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
let vernac_interp ~solve ~abstract cancel nworkers safe_id id
{ indentation; verbose; loc; expr = e; strlen }
@@ -2014,7 +2014,7 @@ and Query : sig
end = struct (* {{{ *)
- module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask)
+ module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) ()
let queue = ref None
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 1716ac0c6..17f90b7b1 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
+module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 9507e90ba..da6a095ab 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -14,7 +14,7 @@ let check_vio (ts,f) =
Stm.set_compilation_hints long_f_dot_v;
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
-module Worker = Spawn.Sync(struct end)
+module Worker = Spawn.Sync ()
module IntOT = struct
type t = int
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 79723431c..b5c5b2b96 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -288,7 +288,7 @@ let usage () =
(Filename.basename Sys.argv.(0))
(Parser.print grammar))
-module Coqide = Spawn.Sync(struct end)
+module Coqide = Spawn.Sync ()
let main =
if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 04:47:52 +0000