diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-10 19:42:09 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-10 19:45:00 +0200 |
commit | 6ac16429294ff3a755c618ece3ba5e22d59e27f9 (patch) | |
tree | c1bf5797cf288b5bd930c58b844ddd97d63fd188 /checker | |
parent | c3c747475f5818445438e779bed0685e01306eff (diff) |
Removing dead code in checker/univ.ml.
Diffstat (limited to 'checker')
-rw-r--r-- | checker/declarations.ml | 1 | ||||
-rw-r--r-- | checker/univ.ml | 29 | ||||
-rw-r--r-- | checker/univ.mli | 5 |
3 files changed, 0 insertions, 35 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index f500693ce..c705a707f 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -442,7 +442,6 @@ let subst_constant_def sub = function | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) (** Local variables and graph *) -type universe_context = Univ.LSet.t * Univ.constraints let body_of_constant cb = match cb.const_body with | Undef _ -> None diff --git a/checker/univ.ml b/checker/univ.ml index d8ee5c35e..e2e40ddc9 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -370,8 +370,6 @@ module Level = struct end -module LSet = Set.Make (Level) - (** Level maps *) module LMap = Map.Make (Level) @@ -381,8 +379,6 @@ type universe_level = Level.t type universe_level_subst_fn = universe_level -> universe_level -type universe_set = LSet.t - (* An algebraic universe [universe] is either a universe variable [Level.t] or a formal universe known to be greater than some universe variables and strictly greater than some (other) universe @@ -1066,31 +1062,6 @@ let merge_constraints c g = type constraints = Constraint.t -module Hconstraint = - Hashcons.Make( - struct - type t = univ_constraint - type u = universe_level -> universe_level - let hashcons hul (l1,k,l2) = (hul l1, k, hul l2) - let equal (l1,k,l2) (l1',k',l2') = - l1 == l1' && k == k' && l2 == l2' - let hash = Hashtbl.hash - end) - -module Hconstraints = - Hashcons.Make( - struct - type t = constraints - type u = univ_constraint -> univ_constraint - let hashcons huc s = - Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty - let equal s s' = - List.for_all2eq (==) - (Constraint.elements s) - (Constraint.elements s') - let hash = Hashtbl.hash - end) - (** A value with universe constraints. *) type 'a constrained = 'a * constraints diff --git a/checker/univ.mli b/checker/univ.mli index b000a7ba2..b2f2c9c18 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -23,11 +23,6 @@ end type universe_level = Level.t (** Alias name. *) -(** Sets of universe levels *) -module LSet : Set.S with type elt = universe_level - -type universe_set = LSet.t - module Universe : sig type t |