diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.mli | 6 | ||||
| -rw-r--r-- | library/globnames.ml | 1 | ||||
| -rw-r--r-- | library/globnames.mli | 7 | ||||
| -rw-r--r-- | library/goptions.ml | 9 | ||||
| -rw-r--r-- | library/libnames.mli | 3 |
5 files changed, 19 insertions, 7 deletions
diff --git a/library/assumptions.mli b/library/assumptions.mli index f91412013..cd08caf73 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Names open Term open Environ @@ -19,8 +20,9 @@ type context_object = | Transparent of constant (** A transparent constant *) (** AssumptionSet.t is a set of [assumption] *) -module OrderedContextObject : Set.OrderedType with type t = context_object -module ContextObjectMap : Map.S with type key = context_object +module ContextObjectSet : Set.S with type elt = context_object +module ContextObjectMap : Map.ExtS + with type key = context_object and module Set := ContextObjectSet (** collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type) *) diff --git a/library/globnames.ml b/library/globnames.ml index a04cdea8c..e80197030 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Errors open Names open Term diff --git a/library/globnames.mli b/library/globnames.mli index 74da2cca8..4bf21cf0a 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Pp open Names open Term @@ -57,10 +58,12 @@ module RefOrdered_env : sig end module Refset : Set.S with type elt = global_reference -module Refmap : Map.S with type key = global_reference +module Refmap : Map.ExtS + with type key = global_reference and module Set := Refset module Refset_env : Set.S with type elt = global_reference -module Refmap_env : Map.S with type key = global_reference +module Refmap_env : Map.ExtS + with type key = global_reference and module Set := Refset_env (** {6 Extended global references } *) diff --git a/library/goptions.ml b/library/goptions.ml index 80539a156..4151e6774 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -192,8 +192,13 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -module OptionMap = - Map.Make (struct type t = option_name let compare = compare end) +module OptionOrd = +struct + type t = option_name + let compare = compare +end + +module OptionMap = Map.Make(OptionOrd) let value_tab = ref OptionMap.empty diff --git a/library/libnames.mli b/library/libnames.mli index 627b8f013..60ec7af79 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Pp open Loc open Names @@ -37,7 +38,7 @@ val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool module Dirset : Set.S with type elt = DirPath.t -module Dirmap : Map.S with type key = DirPath.t +module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset (** {6 Full paths are {e absolute} paths of declarations } *) type full_path |