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/univ.ml | |
| parent | c3c747475f5818445438e779bed0685e01306eff (diff) | |
Removing dead code in checker/univ.ml.
Diffstat (limited to 'checker/univ.ml')
| -rw-r--r-- | checker/univ.ml | 29 |
1 files changed, 0 insertions, 29 deletions
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 |