diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-01 15:01:37 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-01 15:11:22 +0100 |
commit | c8533911300df8d4897a3109ea30d43be7f430eb (patch) | |
tree | 024ea3154461be06aa18ffb8270620d5bdcaa448 | |
parent | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (diff) |
Fix FIXME: use OCaml 4.02 generative functors when available.
4.02.3 has been the minimal OCaml version for a while now.
-rw-r--r-- | engine/evd.ml | 3 | ||||
-rw-r--r-- | engine/geninterp.ml | 4 | ||||
-rw-r--r-- | interp/genintern.ml | 2 | ||||
-rw-r--r-- | lib/cSig.mli | 2 | ||||
-rw-r--r-- | lib/dyn.ml | 2 | ||||
-rw-r--r-- | lib/dyn.mli | 3 | ||||
-rw-r--r-- | lib/exninfo.ml | 2 | ||||
-rw-r--r-- | lib/genarg.ml | 2 | ||||
-rw-r--r-- | lib/spawn.ml | 4 | ||||
-rw-r--r-- | lib/spawn.mli | 4 | ||||
-rw-r--r-- | lib/store.ml | 6 | ||||
-rw-r--r-- | lib/store.mli | 7 | ||||
-rw-r--r-- | library/libobject.ml | 2 | ||||
-rw-r--r-- | library/summary.ml | 2 | ||||
-rw-r--r-- | parsing/pcoq.ml | 4 | ||||
-rw-r--r-- | stm/asyncTaskQueue.ml | 8 | ||||
-rw-r--r-- | stm/asyncTaskQueue.mli | 4 | ||||
-rw-r--r-- | stm/proofworkertop.ml | 2 | ||||
-rw-r--r-- | stm/queryworkertop.ml | 2 | ||||
-rw-r--r-- | stm/stm.ml | 8 | ||||
-rw-r--r-- | stm/tacworkertop.ml | 2 | ||||
-rw-r--r-- | stm/vio_checking.ml | 2 | ||||
-rw-r--r-- | tools/fake_ide.ml | 2 |
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 |